1.1 --- a/src/HOL/Tools/meson.ML Mon Oct 23 11:17:24 2006 +0200
1.2 +++ b/src/HOL/Tools/meson.ML Mon Oct 23 11:17:29 2006 +0200
1.3 @@ -549,14 +549,21 @@
1.4 fun iter_deepen_prolog_tac horns =
1.5 ITER_DEEPEN (has_fewer_prems 1) (prolog_step_tac' horns);
1.6
1.7 -fun iter_deepen_meson_tac ths =
1.8 - MESON (fn cls =>
1.9 - case (gocls (cls@ths)) of
1.10 - [] => no_tac (*no goal clauses*)
1.11 - | goes =>
1.12 - (THEN_ITER_DEEPEN (resolve_tac goes 1)
1.13 - (has_fewer_prems 1)
1.14 - (prolog_step_tac' (make_horns (cls@ths)))));
1.15 +fun iter_deepen_meson_tac ths = MESON
1.16 + (fn cls =>
1.17 + case (gocls (cls@ths)) of
1.18 + [] => no_tac (*no goal clauses*)
1.19 + | goes =>
1.20 + let val horns = make_horns (cls@ths)
1.21 + val _ = if !Output.show_debug_msgs
1.22 + then Output.debug ("meson method called:\n" ^
1.23 + space_implode "\n" (map string_of_thm (cls@ths)) ^
1.24 + "\nclauses:\n" ^
1.25 + space_implode "\n" (map string_of_thm horns))
1.26 + else ()
1.27 + in THEN_ITER_DEEPEN (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns)
1.28 + end
1.29 + );
1.30
1.31 fun meson_claset_tac ths cs =
1.32 SELECT_GOAL (TRY (safe_tac cs) THEN TRYALL (iter_deepen_meson_tac ths));