diff -r 72a31418ff8d -r 82b9feeab1ef src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Jul 23 15:32:30 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Jul 23 15:32:30 2012 +0200
@@ -162,12 +162,11 @@
 
 (* Don't count nested lambdas at the level of formulas, since they are
    quantifiers. *)
-fun formula_has_too_many_lambdas true _ _ = false (*i.e. ho_atp*)
-  | formula_has_too_many_lambdas _ Ts (Abs (_, T, t)) =
-      formula_has_too_many_lambdas false (T :: Ts) t
-  | formula_has_too_many_lambdas _ Ts t =
+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 false Ts) (#2 (strip_comb t))
+      exists (formula_has_too_many_lambdas Ts) (#2 (strip_comb t))
     else
       term_has_too_many_lambdas max_lambda_nesting t
 
@@ -180,7 +179,8 @@
   | apply_depth _ = 0
 
 fun is_formula_too_complex ho_atp t =
-  apply_depth t > max_apply_depth orelse formula_has_too_many_lambdas ho_atp [] t
+  apply_depth t > max_apply_depth orelse
+  (not ho_atp andalso formula_has_too_many_lambdas [] t)
 
 (* FIXME: Extend to "Meson" and "Metis" *)
 val exists_sledgehammer_const =