--- 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 =