# HG changeset patch
# User blanchet
# Date 1355315303 -3600
# Node ID b977b727c7d58cfd7f0d87217dc6738a3296c7f7
# Parent  0b7288aee7514e9a7f8252be8306133216dabfa5
really all facts means really all facts (well, almost)

diff -r 0b7288aee751 -r b977b727c7d5 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Dec 12 13:28:01 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Dec 12 13:28:23 2012 +0100
@@ -154,7 +154,7 @@
         append ["induct", "inducts"]
   |> map (prefix Long_Name.separator)
 
-val max_lambda_nesting = 3 (*only applies if not ho_atp*)
+val max_lambda_nesting = 5 (*only applies if not ho_atp*)
 
 fun term_has_too_many_lambdas max (t1 $ t2) =
     exists (term_has_too_many_lambdas max) [t1, t2]
@@ -174,7 +174,7 @@
 
 (* The max apply depth of any "metis" call in "Metis_Examples" (on 2007-10-31)
    was 11. *)
-val max_apply_depth = 15
+val max_apply_depth = 18
 
 fun apply_depth (f $ t) = Int.max (apply_depth f, apply_depth t + 1)
   | apply_depth (Abs (_, _, t)) = apply_depth t
@@ -229,7 +229,6 @@
   end
 
 fun is_theorem_bad_for_atps ho_atp th =
-  is_likely_tautology_or_too_meta th orelse
   let val t = prop_of th in
     is_formula_too_complex ho_atp t orelse
     exists_type type_has_top_sort t orelse exists_technical_const t orelse
@@ -439,7 +438,9 @@
             #> fold_rev (fn th => fn (j, (multis, unis)) =>
                    (j - 1,
                     if not (member Thm.eq_thm_prop add_ths th) andalso
-                       is_theorem_bad_for_atps ho_atp th then
+                       is_likely_tautology_or_too_meta th orelse
+                       (not really_all andalso
+                        is_theorem_bad_for_atps ho_atp th) then
                       (multis, unis)
                     else
                       let