--- a/ProgTutorial/Package/Ind_Code.thy	Mon Apr 13 08:30:48 2009 +0000
+++ b/ProgTutorial/Package/Ind_Code.thy	Wed Apr 15 13:11:08 2009 +0000
@@ -50,7 +50,7 @@
   val arg = ((@{binding "My_True"}, NoSyn), @{term True})
   val (def, lthy') = make_defn arg lthy 
 in
-  warning (str_of_thm_no_vars lthy' def); lthy'
+  writeln (str_of_thm_no_vars lthy' def); lthy'
 end *}
 
 text {*
@@ -117,7 +117,7 @@
 let
   val def = defn_aux lthy eo_orules eo_preds (e_pred, e_arg_tys)
 in
-  warning (Syntax.string_of_term lthy def); lthy
+  writeln (Syntax.string_of_term lthy def); lthy
 end *}
 
 text {*
@@ -133,7 +133,7 @@
 *}
 
 local_setup %gray{* fn lthy =>
- (warning (Syntax.string_of_term lthy
+ (writeln (Syntax.string_of_term lthy
     (defn_aux lthy fresh_orules [fresh_pred] (fresh_pred, fresh_arg_tys)));
   lthy) *}
 
@@ -182,7 +182,7 @@
   val (defs, lthy') = 
     defns eo_rules eo_preds eo_prednames eo_mxs eo_arg_tyss lthy
 in
-  warning (str_of_thms_no_vars lthy' defs); lthy
+  writeln (str_of_thms_no_vars lthy' defs); lthy
 end *}
 
 text {*
@@ -391,7 +391,7 @@
   val intro = 
       prove_ind lthy eo_defs srules cnewpreds ((e_pred, newpred), e_arg_tys)
 in
-  warning (str_of_thm lthy intro); lthy
+  writeln (str_of_thm lthy intro); lthy
 end *}
 
 text {*
@@ -450,7 +450,7 @@
 let 
   val ind_thms = inds eo_rules eo_defs eo_preds eo_arg_tyss lthy
 in
-  warning (str_of_thms lthy ind_thms); lthy
+  writeln (str_of_thms lthy ind_thms); lthy
 end *}
 
 
@@ -516,7 +516,7 @@
   val ctrms = [@{cterm \"a::nat\"}, @{cterm \"b::nat\"}, @{cterm \"c::nat\"}]
   val new_thm = all_elims ctrms @{thm all_elims_test}
 in
-  warning (str_of_thm_no_vars @{context} new_thm)
+  writeln (str_of_thm_no_vars @{context} new_thm)
 end"
   "P a b c"}
 
@@ -529,7 +529,7 @@
   @{thm [source] imp_elims_test}:
 
   @{ML_response_fake [display, gray]
-"warning (str_of_thm_no_vars @{context} 
+"writeln (str_of_thm_no_vars @{context} 
             (imp_elims @{thms imp_elims_test'} @{thm imp_elims_test}))"
   "C"}
 
@@ -611,7 +611,7 @@
 in 
   s |> separate "\n"
     |> implode
-    |> warning
+    |> writeln
 end*}
 text_raw{*
 \end{isabelle}