# HG changeset patch
# User blanchet
# Date 1378821411 -7200
# Node ID f99ee3adb81d40f36eb2205c50010b1ae75a52ff
# Parent  412f8c590c6cd55b291a0712e768ec43a92aee30
got rid of old, needless logic

diff -r 412f8c590c6c -r f99ee3adb81d src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Sep 10 15:56:51 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Sep 10 15:56:51 2013 +0200
@@ -195,36 +195,6 @@
         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",
@@ -496,9 +466,7 @@
             #> 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 orelse
-                        (not generous andalso
-                         is_too_complex ho_atp (prop_of th))) then
+                       (is_likely_tautology_too_meta_or_too_technical th) then
                       accum
                     else
                       let