# HG changeset patch
# User blanchet
# Date 1378901244 -7200
# Node ID 6e817f070f66e4c854ffb99e529fc20c4d6cd1e0
# Parent  1eb7c65b526cf2786d2c94eb5a5716f64bc1f4f3
reintroduced half of f99ee3adb81d -- that part definitely looks useless (and is inefficient)

diff -r 1eb7c65b526c -r 6e817f070f66 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Sep 11 14:07:24 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Sep 11 14:07:24 2013 +0200
@@ -191,24 +191,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
@@ -217,9 +199,7 @@
   | 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)
+fun is_too_complex ho_atp t = apply_depth t > max_apply_depth
 
 (* FIXME: Ad hoc list *)
 val technical_prefixes =