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));