src/HOL/Tools/meson.ML
changeset 38802 a925c0ee42f7
parent 38795 848be46708dc
child 38806 0aafc7e81056
     1.1 --- a/src/HOL/Tools/meson.ML	Fri Aug 27 15:46:08 2010 +0200
     1.2 +++ b/src/HOL/Tools/meson.ML	Fri Aug 27 16:29:12 2010 +0200
     1.3 @@ -50,6 +50,9 @@
     1.4  val max_clauses_default = 60;
     1.5  val (max_clauses, setup) = Attrib.config_int "max_clauses" (K max_clauses_default);
     1.6  
     1.7 +(*No known example (on 1-5-2007) needs even thirty*)
     1.8 +val iter_deepen_limit = 50;
     1.9 +
    1.10  val disj_forward = @{thm disj_forward};
    1.11  val disj_forward2 = @{thm disj_forward2};
    1.12  val make_pos_rule = @{thm make_pos_rule};
    1.13 @@ -640,7 +643,7 @@
    1.14      end;
    1.15  
    1.16  fun iter_deepen_prolog_tac horns =
    1.17 -    ITER_DEEPEN (has_fewer_prems 1) (prolog_step_tac' horns);
    1.18 +    ITER_DEEPEN iter_deepen_limit (has_fewer_prems 1) (prolog_step_tac' horns);
    1.19  
    1.20  fun iter_deepen_meson_tac ctxt ths = ctxt |> MESON make_clauses
    1.21    (fn cls =>
    1.22 @@ -653,7 +656,10 @@
    1.23              cat_lines ("meson method called:" ::
    1.24                map (Display.string_of_thm ctxt) (cls @ ths) @
    1.25                ["clauses:"] @ map (Display.string_of_thm ctxt) horns))
    1.26 -        in THEN_ITER_DEEPEN (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns) end));
    1.27 +        in
    1.28 +          THEN_ITER_DEEPEN iter_deepen_limit
    1.29 +            (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns)
    1.30 +        end));
    1.31  
    1.32  fun meson_tac ctxt ths =
    1.33    SELECT_GOAL (TRY (safe_tac (claset_of ctxt)) THEN TRYALL (iter_deepen_meson_tac ctxt ths));