--- a/ProgTutorial/Package/Ind_Code.thy	Mon Aug 03 13:53:04 2009 +0200
+++ b/ProgTutorial/Package/Ind_Code.thy	Mon Aug 03 14:01:57 2009 +0200
@@ -50,7 +50,7 @@
   val arg = ((@{binding "My_True"}, NoSyn), @{term True})
   val (def, lthy') = make_defn arg lthy 
 in
-  writeln (string_of_thm_no_vars lthy' def); lthy'
+  tracing (string_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
-  writeln (Syntax.string_of_term lthy def); lthy
+  tracing (Syntax.string_of_term lthy def); lthy
 end *}
 
 text {*
@@ -137,7 +137,7 @@
   val def = defn_aux lthy fresh_orules 
                              [fresh_pred] (fresh_pred, fresh_arg_tys)
 in
-  writeln (Syntax.string_of_term lthy def); lthy
+  tracing (Syntax.string_of_term lthy def); lthy
 end *}
 
 
@@ -187,7 +187,7 @@
   val (defs, lthy') = 
     defns eo_rules eo_preds eo_prednames eo_mxs eo_arg_tyss lthy
 in
-  writeln (string_of_thms_no_vars lthy' defs); lthy
+  tracing (string_of_thms_no_vars lthy' defs); lthy
 end *}
 
 text {*
@@ -401,7 +401,7 @@
   val intro = 
       prove_ind lthy eo_defs srules cnewpreds ((e_pred, newpred), e_arg_tys)
 in
-  writeln (string_of_thm lthy intro); lthy
+  tracing (string_of_thm lthy intro); lthy
 end *}
 
 text {*
@@ -460,7 +460,7 @@
 let 
   val ind_thms = inds eo_rules eo_defs eo_preds eo_arg_tyss lthy
 in
-  writeln (string_of_thms lthy ind_thms); lthy
+  tracing (string_of_thms lthy ind_thms); lthy
 end *}
 
 
@@ -526,7 +526,7 @@
   val ctrms = [@{cterm \"a::nat\"}, @{cterm \"b::nat\"}, @{cterm \"c::nat\"}]
   val new_thm = all_elims ctrms @{thm all_elims_test}
 in
-  writeln (string_of_thm_no_vars @{context} new_thm)
+  tracing (string_of_thm_no_vars @{context} new_thm)
 end"
   "P a b c"}
 
@@ -542,7 +542,7 @@
 "let
   val res = imp_elims @{thms imp_elims_test'} @{thm imp_elims_test}
 in
-  writeln (string_of_thm_no_vars @{context} res)
+  tracing (string_of_thm_no_vars @{context} res)
 end"
   "C"}