# HG changeset patch
# User blanchet
# Date 1378901244 -7200
# Node ID 1eb7c65b526cf2786d2c94eb5a5716f64bc1f4f3
# Parent  129bd52a5e5f01e4e9c5c5a6d81a24db9396426d
reverted f99ee3adb81d -- that old logic seems to make a difference still today

diff -r 129bd52a5e5f -r 1eb7c65b526c src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Sep 11 11:38:07 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Sep 11 14:07:24 2013 +0200
@@ -191,6 +191,36 @@
         append ["induct", "inducts"]
   |> map (prefix Long_Name.separator)
 
+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]
+  | term_has_too_many_lambdas max (Abs (_, _, t)) =
+    max = 0 orelse term_has_too_many_lambdas (max - 1) t
+  | term_has_too_many_lambdas _ _ = false
+
+(* Don't count nested lambdas at the level of formulas, since they are
+   quantifiers. *)
+fun formula_has_too_many_lambdas Ts (Abs (_, T, t)) =
+    formula_has_too_many_lambdas (T :: Ts) t
+  | formula_has_too_many_lambdas Ts t =
+    if member (op =) [HOLogic.boolT, propT] (fastype_of1 (Ts, t)) then
+      exists (formula_has_too_many_lambdas Ts) (#2 (strip_comb t))
+    else
+      term_has_too_many_lambdas max_lambda_nesting t
+
+(* The maximum apply depth of any "metis" call in "Metis_Examples" (on
+   2007-10-31) was 11. *)
+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
+  | apply_depth _ = 0
+
+fun is_too_complex ho_atp t =
+  apply_depth t > max_apply_depth orelse
+  (not ho_atp andalso formula_has_too_many_lambdas [] t)
+
 (* FIXME: Ad hoc list *)
 val technical_prefixes =
   ["ATP", "Code_Evaluation", "Datatype", "Enum", "Lazy_Sequence",
@@ -473,7 +503,9 @@
             #> fold_rev (fn th => fn (j, accum) =>
                    (j - 1,
                     if not (member Thm.eq_thm_prop add_ths th) andalso
-                       is_likely_tautology_too_meta_or_too_technical th then
+                       (is_likely_tautology_too_meta_or_too_technical th orelse
+                        (not generous andalso
+                         is_too_complex ho_atp (prop_of th))) then
                       accum
                     else
                       let