--- a/ProgTutorial/Package/Ind_Code.thy	Sat May 09 18:50:01 2009 +0200
+++ b/ProgTutorial/Package/Ind_Code.thy	Sun May 17 16:22:27 2009 +0200
@@ -50,7 +50,7 @@
   val arg = ((@{binding "My_True"}, NoSyn), @{term True})
   val (def, lthy') = make_defn arg lthy 
 in
-  writeln (str_of_thm_no_vars lthy' def); lthy'
+  writeln (string_of_thm_no_vars lthy' def); lthy'
 end *}
 
 text {*
@@ -182,7 +182,7 @@
   val (defs, lthy') = 
     defns eo_rules eo_preds eo_prednames eo_mxs eo_arg_tyss lthy
 in
-  writeln (str_of_thms_no_vars lthy' defs); lthy
+  writeln (string_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
-  writeln (str_of_thm lthy intro); lthy
+  writeln (string_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
-  writeln (str_of_thms lthy ind_thms); lthy
+  writeln (string_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
-  writeln (str_of_thm_no_vars @{context} new_thm)
+  writeln (string_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]
-"writeln (str_of_thm_no_vars @{context} 
+"writeln (string_of_thm_no_vars @{context} 
             (imp_elims @{thms imp_elims_test'} @{thm imp_elims_test}))"
   "C"}
 
@@ -604,10 +604,10 @@
 *}
 ML{*fun chop_print params1 params2 prems1 prems2 ctxt =
 let 
-  val s = ["Params1 from the rule:", str_of_cterms ctxt params1] 
-        @ ["Params2 from the predicate:", str_of_cterms ctxt params2] 
-        @ ["Prems1 from the rule:"] @ (map (str_of_thm ctxt) prems1) 
-        @ ["Prems2 from the predicate:"] @ (map (str_of_thm ctxt) prems2) 
+  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) 
 in 
   s |> separate "\n"
     |> implode