diff -r 319a28dd3564 -r a925c0ee42f7 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Fri Aug 27 15:46:08 2010 +0200
+++ b/src/HOL/Tools/meson.ML	Fri Aug 27 16:29:12 2010 +0200
@@ -50,6 +50,9 @@
 val max_clauses_default = 60;
 val (max_clauses, setup) = Attrib.config_int "max_clauses" (K max_clauses_default);
 
+(*No known example (on 1-5-2007) needs even thirty*)
+val iter_deepen_limit = 50;
+
 val disj_forward = @{thm disj_forward};
 val disj_forward2 = @{thm disj_forward2};
 val make_pos_rule = @{thm make_pos_rule};
@@ -640,7 +643,7 @@
     end;
 
 fun iter_deepen_prolog_tac horns =
-    ITER_DEEPEN (has_fewer_prems 1) (prolog_step_tac' horns);
+    ITER_DEEPEN iter_deepen_limit (has_fewer_prems 1) (prolog_step_tac' horns);
 
 fun iter_deepen_meson_tac ctxt ths = ctxt |> MESON make_clauses
   (fn cls =>
@@ -653,7 +656,10 @@
             cat_lines ("meson method called:" ::
               map (Display.string_of_thm ctxt) (cls @ ths) @
               ["clauses:"] @ map (Display.string_of_thm ctxt) horns))
-        in THEN_ITER_DEEPEN (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns) end));
+        in
+          THEN_ITER_DEEPEN iter_deepen_limit
+            (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns)
+        end));
 
 fun meson_tac ctxt ths =
   SELECT_GOAL (TRY (safe_tac (claset_of ctxt)) THEN TRYALL (iter_deepen_meson_tac ctxt ths));