1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Sep 11 14:07:24 2013 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Sep 11 14:07:24 2013 +0200
     1.3 @@ -447,10 +447,21 @@
     1.4  
     1.5  fun fact_of_raw_fact ((name, stature), th) = ((name (), stature), th)
     1.6  
     1.7 +fun fact_count facts = Facts.fold_static (K (Integer.add 1)) facts 0
     1.8 +
     1.9 +(* gracefully handle huge background theories *)
    1.10 +val max_facts_for_complex_check = 25000
    1.11 +
    1.12  fun all_facts ctxt generous ho_atp reserved add_ths chained css =
    1.13    let
    1.14      val thy = Proof_Context.theory_of ctxt
    1.15      val global_facts = Global_Theory.facts_of thy
    1.16 +    val is_too_complex =
    1.17 +      if generous orelse
    1.18 +         fact_count global_facts >= max_facts_for_complex_check then
    1.19 +        K false
    1.20 +      else
    1.21 +        is_too_complex ho_atp
    1.22      val local_facts = Proof_Context.facts_of ctxt
    1.23      val named_locals = local_facts |> Facts.dest_static []
    1.24      val assms = Assumption.all_assms_of ctxt
    1.25 @@ -484,8 +495,7 @@
    1.26                     (j - 1,
    1.27                      if not (member Thm.eq_thm_prop add_ths th) andalso
    1.28                         (is_likely_tautology_too_meta_or_too_technical th orelse
    1.29 -                        (not generous andalso
    1.30 -                         is_too_complex ho_atp (prop_of th))) then
    1.31 +                        is_too_complex (prop_of th)) then
    1.32                        accum
    1.33                      else
    1.34                        let