--- a/ProgTutorial/Tactical.thy	Wed Aug 05 08:58:28 2009 +0200
+++ b/ProgTutorial/Tactical.thy	Wed Aug 05 09:24:18 2009 +0200
@@ -551,13 +551,13 @@
   val string_of_prems = string_of_thms_no_vars context prems   
   val string_of_schms = string_of_cterms context (map fst (snd schematics))    
  
-  val _ = (tracing ("params: " ^ string_of_params);
-           tracing ("schematics: " ^ string_of_schms);
-           tracing ("assumptions: " ^ string_of_asms);
-           tracing ("conclusion: " ^ string_of_concl);
-           tracing ("premises: " ^ string_of_prems))
+  val strs = ["params: " ^ string_of_params,
+              "schematics: " ^ string_of_schms,
+              "assumptions: " ^ string_of_asms,
+              "conclusion: " ^ string_of_concl,
+              "premises: " ^ string_of_prems]
 in
-  all_tac 
+  tracing (cat_lines strs); all_tac 
 end*}
 
 text_raw{*