--- a/ProgTutorial/Package/Ind_Code.thy	Mon Mar 23 12:13:33 2009 +0100
+++ b/ProgTutorial/Package/Ind_Code.thy	Mon Mar 23 18:17:24 2009 +0100
@@ -97,7 +97,7 @@
   val arg =  ((@{binding "MyTrue"}, NoSyn), @{term True})
   val (def, lthy') = make_defs arg lthy 
 in
-  warning (str_of_thm lthy' def); lthy'
+  warning (str_of_thm_no_vars lthy' def); lthy'
 end *}
 
 text {*
@@ -218,7 +218,7 @@
   val arg_tyss = [[@{typ "nat"}], [@{typ "nat"}]]
   val (defs, lthy') = definitions rules preds prednames syns arg_tyss lthy
 in
-  warning (str_of_thms lthy' defs); lthy'
+  warning (str_of_thms_no_vars lthy' defs); lthy'
 end *}
 
 text {*
@@ -413,7 +413,7 @@
   val intro = 
     prove_induction lthy defs srules cnewpreds ((pred, newpred), arg_tys)
 in
-  warning (str_of_thm_raw lthy intro); lthy
+  warning (str_of_thm lthy intro); lthy
 end *} 
 
 text {*
@@ -477,7 +477,7 @@
   val tyss = [[@{typ "nat"}], [@{typ "nat"}]]
   val ind_thms = inductions rules defs preds tyss lthy
 in
-  warning (str_of_thms_raw lthy ind_thms); lthy
+  warning (str_of_thms lthy ind_thms); lthy
 end *}
 
 
@@ -530,7 +530,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 @{context} new_thm)
+  warning (str_of_thm_no_vars @{context} new_thm)
 end"
   "P a b c"}
 
@@ -538,7 +538,7 @@
   For example 
 
   @{ML_response_fake [display, gray]
-"warning (str_of_thm @{context} 
+"warning (str_of_thm_no_vars @{context} 
             (imp_elims @{thms imp_elims_test'} @{thm imp_elims_test}))"
   "C"}
 *}
@@ -571,7 +571,7 @@
 ML {*
 fun chop_print_tac2 ctxt prems =
 let
-  val _ = warning (commas (map (str_of_thm ctxt) prems))
+  val _ = warning (commas (map (str_of_thm_no_vars ctxt) prems))
 in
    all_tac
 end