--- a/ProgTutorial/Tactical.thy	Tue Jun 14 22:09:40 2011 +0100
+++ b/ProgTutorial/Tactical.thy	Fri Jun 17 16:58:05 2011 +0100
@@ -775,20 +775,12 @@
   is similar to @{ML RS}, but takes an additional number as argument. This 
   number makes explicit which premise should be instantiated. 
 
-  To improve readability of the theorems we shall produce below, we will use the
-  function @{ML no_vars} from Section~\ref{sec:printing}, which transforms
-  schematic variables into free ones.  Using this function for the first @{ML
-  RS}-expression above produces the more readable result:
-
-  @{ML_response_fake [display,gray]
-  "no_vars @{context} (@{thm disjI1} RS @{thm conjI})" "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> (P \<or> Qa) \<and> Q"}
-
   If you want to instantiate more than one premise of a theorem, you can use 
   the function @{ML_ind MRS in Drule}:
 
   @{ML_response_fake [display,gray]
-  "no_vars @{context} ([@{thm disjI1}, @{thm disjI2}] MRS @{thm conjI})" 
-  "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> (P \<or> Qa) \<and> (Pa \<or> Q)"}
+  "[@{thm disjI1}, @{thm disjI2}] MRS @{thm conjI}" 
+  "\<lbrakk>?P2; ?Q1\<rbrakk> \<Longrightarrow> (?P2 \<or> ?Q2) \<and> (?P1 \<or> ?Q1)"}
 
   If you need to instantiate lists of theorems, you can use the
   functions @{ML_ind RL in Drule} and @{ML_ind MRL in Drule}. For 
@@ -800,12 +792,12 @@
   val list1 = [@{thm impI}, @{thm disjI2}]
   val list2 = [@{thm conjI}, @{thm disjI1}]
 in
-  map (no_vars @{context}) (list1 RL list2)
+  list1 RL list2
 end" 
-"[\<lbrakk>P \<Longrightarrow> Q; Qa\<rbrakk> \<Longrightarrow> (P \<longrightarrow> Q) \<and> Qa,
- \<lbrakk>Q; Qa\<rbrakk> \<Longrightarrow> (P \<or> Q) \<and> Qa,
- (P \<Longrightarrow> Q) \<Longrightarrow> (P \<longrightarrow> Q) \<or> Qa,
- Q \<Longrightarrow> (P \<or> Q) \<or> Qa]"}
+"[\<lbrakk>?P1 \<Longrightarrow> ?Q1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<longrightarrow> ?Q1) \<and> ?Q, 
+ \<lbrakk>?Q1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q,
+ (?P1 \<Longrightarrow> ?Q1) \<Longrightarrow> (?P1 \<longrightarrow> ?Q1) \<or> ?Q, 
+ ?Q1 \<Longrightarrow> (?P1 \<or> ?Q1) \<or> ?Q]"}
 
   \begin{readmore}
   The combinators for instantiating theorems with other theorems are