--- a/ProgTutorial/Tactical.thy	Mon Apr 13 08:30:48 2009 +0000
+++ b/ProgTutorial/Tactical.thy	Wed Apr 15 13:11:08 2009 +0000
@@ -210,7 +210,7 @@
 
 ML{*fun my_print_tac ctxt thm =
 let
-  val _ = warning (str_of_thm_no_vars ctxt thm)
+  val _ = writeln (str_of_thm_no_vars ctxt thm)
 in 
   Seq.single thm
 end*}
@@ -537,11 +537,11 @@
   val str_of_prems = str_of_thms_no_vars context prems   
   val str_of_schms = str_of_cterms context (snd schematics)    
  
-  val _ = (warning ("params: " ^ str_of_params);
-           warning ("schematics: " ^ str_of_schms);
-           warning ("assumptions: " ^ str_of_asms);
-           warning ("conclusion: " ^ str_of_concl);
-           warning ("premises: " ^ str_of_prems))
+  val _ = (writeln ("params: " ^ str_of_params);
+           writeln ("schematics: " ^ str_of_schms);
+           writeln ("assumptions: " ^ str_of_asms);
+           writeln ("conclusion: " ^ str_of_concl);
+           writeln ("premises: " ^ str_of_prems))
 in
   no_tac 
 end*}
@@ -583,7 +583,7 @@
   expects that the subgoal is solved completely.  Since in the function @{ML
   sp_tac} we returned the tactic @{ML no_tac}, the subproof obviously
   fails. The question-mark allows us to recover from this failure in a
-  graceful manner so that the warning messages are not overwritten by an 
+  graceful manner so that the output messages are not overwritten by an 
   ``empty sequence'' error message.
 
   If we continue the proof script by applying the @{text impI}-rule
@@ -1172,7 +1172,7 @@
 in
   s |> separate "\n"
     |> implode
-    |> warning
+    |> writeln
 end*}
 text_raw {* 
 \end{isabelle}
@@ -1494,7 +1494,7 @@
 ML %linenosgray{*fun fail_sp_aux simpset redex = 
 let
   val ctxt = Simplifier.the_context simpset
-  val _ = warning ("The redex: " ^ (str_of_cterm ctxt redex))
+  val _ = writeln ("The redex: " ^ (str_of_cterm ctxt redex))
 in
   NONE
 end*}
@@ -1565,7 +1565,7 @@
 ML{*fun fail_sp_aux' simpset redex = 
 let
   val ctxt = Simplifier.the_context simpset
-  val _ = warning ("The redex: " ^ (Syntax.string_of_term ctxt redex))
+  val _ = writeln ("The redex: " ^ (Syntax.string_of_term ctxt redex))
 in
   NONE
 end*}