--- a/ProgTutorial/Package/Ind_Code.thy	Mon Jul 19 15:44:13 2010 +0100
+++ b/ProgTutorial/Package/Ind_Code.thy	Tue Jul 20 13:34:44 2010 +0100
@@ -162,7 +162,7 @@
   val (defs, lthy') = 
     defns eo_rules eo_preds eo_prednames eo_mxs eo_arg_tyss lthy
 in
-  tracing (string_of_thms_no_vars lthy' defs); lthy
+  pwriteln (pretty_thms_no_vars lthy' defs); lthy
 end *}
 
 text {*
@@ -381,7 +381,7 @@
   val intro = 
       prove_ind lthy eo_defs srules cnewpreds ((e_pred, newpred), e_arg_tys)
 in
-  tracing (string_of_thm lthy intro); lthy
+  pwriteln (pretty_thm lthy intro); lthy
 end *}
 
 text {*
@@ -440,7 +440,7 @@
 let 
   val ind_thms = inds eo_rules eo_defs eo_preds eo_arg_tyss lthy
 in
-  tracing (string_of_thms lthy ind_thms); lthy
+  pwriteln (pretty_thms lthy ind_thms); lthy
 end *}
 
 
@@ -506,7 +506,7 @@
   val ctrms = [@{cterm \"a::nat\"}, @{cterm \"b::nat\"}, @{cterm \"c::nat\"}]
   val new_thm = all_elims ctrms @{thm all_elims_test}
 in
-  tracing (string_of_thm_no_vars @{context} new_thm)
+  pwriteln (pretty_thm_no_vars @{context} new_thm)
 end"
   "P a b c"}
 
@@ -522,7 +522,7 @@
 "let
   val res = imp_elims @{thms imp_elims_test'} @{thm imp_elims_test}
 in
-  tracing (string_of_thm_no_vars @{context} res)
+  pwriteln (pretty_thm_no_vars @{context} res)
 end"
   "C"}
 
@@ -590,13 +590,13 @@
 *}
 ML{*fun chop_print params1 params2 prems1 prems2 ctxt =
 let 
- val s = ["Params1 from the rule:", string_of_cterms ctxt params1] 
-       @ ["Params2 from the predicate:", string_of_cterms ctxt params2] 
-       @ ["Prems1 from the rule:"] @ (map (string_of_thm ctxt) prems1) 
-       @ ["Prems2 from the predicate:"] @ (map (string_of_thm ctxt) prems2) 
+ val pps = [Pretty.big_list "Params1 from the rule:" (map (pretty_cterm ctxt) params1), 
+            Pretty.big_list "Params2 from the predicate:" (map (pretty_cterm ctxt) params2), 
+            Pretty.big_list "Prems1 from the rule:" (map (pretty_thm ctxt) prems1),
+            Pretty.big_list "Prems2 from the predicate:" (map (pretty_thm ctxt) prems2)] 
 in 
-  s |> cat_lines
-    |> tracing
+  pps |> Pretty.chunks
+      |> tracing o Pretty.string_of
 end*}
 text_raw{*
 \end{isabelle}