--- a/ProgTutorial/Tactical.thy	Mon Mar 23 12:13:33 2009 +0100
+++ b/ProgTutorial/Tactical.thy	Mon Mar 23 18:17:24 2009 +0100
@@ -209,7 +209,7 @@
 
 ML{*fun my_print_tac ctxt thm =
 let
-  val _ = warning (str_of_thm ctxt thm)
+  val _ = warning (str_of_thm_no_vars ctxt thm)
 in 
   Seq.single thm
 end*}
@@ -325,7 +325,7 @@
 
 *}
 
-section {* Simple Tactics *}
+section {* Simple Tactics\label{sec:simpletacs} *}
 
 text {*
   Let us start with explaining the simple tactic @{ML print_tac}, which is quite useful 
@@ -546,7 +546,7 @@
   val str_of_params = str_of_cterms context params
   val str_of_asms = str_of_cterms context asms
   val str_of_concl = str_of_cterm context concl
-  val str_of_prems = str_of_thms context prems   
+  val str_of_prems = str_of_thms_no_vars context prems   
   val str_of_schms = str_of_cterms context (snd schematics)    
  
   val _ = (warning ("params: " ^ str_of_params);
@@ -1143,7 +1143,7 @@
   val {simps, congs, procs, ...} = MetaSimplifier.dest_ss ss
 
   fun name_thm (nm, thm) =
-      "  " ^ nm ^ ": " ^ (str_of_thm ctxt thm)
+      "  " ^ nm ^ ": " ^ (str_of_thm_no_vars ctxt thm)
   fun name_ctrm (nm, ctrm) =
       "  " ^ nm ^ ": " ^ (str_of_cterms ctxt ctrm)