# HG changeset patch
# User paulson
# Date 1161595049 -7200
# Node ID 2c9f73fa973c3552cc38633b80bb5bfe92797082
# Parent  7e18c11e626791af621c43e64cfe46616e33153d
Improved tracing

diff -r 7e18c11e6267 -r 2c9f73fa973c src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Mon Oct 23 11:17:24 2006 +0200
+++ b/src/HOL/Tools/meson.ML	Mon Oct 23 11:17:29 2006 +0200
@@ -549,14 +549,21 @@
 fun iter_deepen_prolog_tac horns =
     ITER_DEEPEN (has_fewer_prems 1) (prolog_step_tac' horns);
 
-fun iter_deepen_meson_tac ths =
-  MESON (fn cls =>
-           case (gocls (cls@ths)) of
-           	[] => no_tac  (*no goal clauses*)
-              | goes => 
-		 (THEN_ITER_DEEPEN (resolve_tac goes 1)
-				   (has_fewer_prems 1)
-				   (prolog_step_tac' (make_horns (cls@ths)))));
+fun iter_deepen_meson_tac ths = MESON 
+ (fn cls =>
+      case (gocls (cls@ths)) of
+	   [] => no_tac  (*no goal clauses*)
+	 | goes => 
+	     let val horns = make_horns (cls@ths)
+	         val _ = if !Output.show_debug_msgs 
+	                 then Output.debug ("meson method called:\n" ^ 
+	     	                  space_implode "\n" (map string_of_thm (cls@ths)) ^ 
+	     	                  "\nclauses:\n" ^ 
+	     	                  space_implode "\n" (map string_of_thm horns))
+	     	         else ()
+	     in THEN_ITER_DEEPEN (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns)
+	     end
+ );
 
 fun meson_claset_tac ths cs =
   SELECT_GOAL (TRY (safe_tac cs) THEN TRYALL (iter_deepen_meson_tac ths));