1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Jul 23 15:32:30 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Jul 23 15:32:30 2012 +0200
     1.3 @@ -162,12 +162,11 @@
     1.4  
     1.5  (* Don't count nested lambdas at the level of formulas, since they are
     1.6     quantifiers. *)
     1.7 -fun formula_has_too_many_lambdas true _ _ = false (*i.e. ho_atp*)
     1.8 -  | formula_has_too_many_lambdas _ Ts (Abs (_, T, t)) =
     1.9 -      formula_has_too_many_lambdas false (T :: Ts) t
    1.10 -  | formula_has_too_many_lambdas _ Ts t =
    1.11 +fun formula_has_too_many_lambdas Ts (Abs (_, T, t)) =
    1.12 +    formula_has_too_many_lambdas (T :: Ts) t
    1.13 +  | formula_has_too_many_lambdas Ts t =
    1.14      if member (op =) [HOLogic.boolT, propT] (fastype_of1 (Ts, t)) then
    1.15 -      exists (formula_has_too_many_lambdas false Ts) (#2 (strip_comb t))
    1.16 +      exists (formula_has_too_many_lambdas Ts) (#2 (strip_comb t))
    1.17      else
    1.18        term_has_too_many_lambdas max_lambda_nesting t
    1.19  
    1.20 @@ -180,7 +179,8 @@
    1.21    | apply_depth _ = 0
    1.22  
    1.23  fun is_formula_too_complex ho_atp t =
    1.24 -  apply_depth t > max_apply_depth orelse formula_has_too_many_lambdas ho_atp [] t
    1.25 +  apply_depth t > max_apply_depth orelse
    1.26 +  (not ho_atp andalso formula_has_too_many_lambdas [] t)
    1.27  
    1.28  (* FIXME: Extend to "Meson" and "Metis" *)
    1.29  val exists_sledgehammer_const =