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 @@ -191,24 +191,6 @@
     1.4          append ["induct", "inducts"]
     1.5    |> map (prefix Long_Name.separator)
     1.6  
     1.7 -val max_lambda_nesting = 5 (*only applies if not ho_atp*)
     1.8 -
     1.9 -fun term_has_too_many_lambdas max (t1 $ t2) =
    1.10 -    exists (term_has_too_many_lambdas max) [t1, t2]
    1.11 -  | term_has_too_many_lambdas max (Abs (_, _, t)) =
    1.12 -    max = 0 orelse term_has_too_many_lambdas (max - 1) t
    1.13 -  | term_has_too_many_lambdas _ _ = false
    1.14 -
    1.15 -(* Don't count nested lambdas at the level of formulas, since they are
    1.16 -   quantifiers. *)
    1.17 -fun formula_has_too_many_lambdas Ts (Abs (_, T, t)) =
    1.18 -    formula_has_too_many_lambdas (T :: Ts) t
    1.19 -  | formula_has_too_many_lambdas Ts t =
    1.20 -    if member (op =) [HOLogic.boolT, propT] (fastype_of1 (Ts, t)) then
    1.21 -      exists (formula_has_too_many_lambdas Ts) (#2 (strip_comb t))
    1.22 -    else
    1.23 -      term_has_too_many_lambdas max_lambda_nesting t
    1.24 -
    1.25  (* The maximum apply depth of any "metis" call in "Metis_Examples" (on
    1.26     2007-10-31) was 11. *)
    1.27  val max_apply_depth = 18
    1.28 @@ -217,9 +199,7 @@
    1.29    | apply_depth (Abs (_, _, t)) = apply_depth t
    1.30    | apply_depth _ = 0
    1.31  
    1.32 -fun is_too_complex ho_atp t =
    1.33 -  apply_depth t > max_apply_depth orelse
    1.34 -  (not ho_atp andalso formula_has_too_many_lambdas [] t)
    1.35 +fun is_too_complex ho_atp t = apply_depth t > max_apply_depth
    1.36  
    1.37  (* FIXME: Ad hoc list *)
    1.38  val technical_prefixes =