--- a/ProgTutorial/Tactical.thy	Tue Mar 31 20:31:18 2009 +0100
+++ b/ProgTutorial/Tactical.thy	Wed Apr 01 12:26:56 2009 +0100
@@ -1652,11 +1652,10 @@
   @{text num} (Line 3), and then generates the meta-equation @{text "t \<equiv> num"} 
   (Line 4), which it proves by the arithmetic tactic in Line 6. 
 
-  For our purpose at the moment, proving the meta-equation using 
-  @{ML Arith_Data.arith_tac} is
-  fine, but there is also an alternative employing the simplifier with a very
-  restricted simpset. For the kind of lemmas we want to prove, the simpset
-  @{text "num_ss"} in the code will suffice.
+  For our purpose at the moment, proving the meta-equation using @{ML
+  arith_tac in Arith_Data} is fine, but there is also an alternative employing
+  the simplifier with a special simpset. For the kind of lemmas we
+  want to prove here, the simpset @{text "num_ss"} should suffice.
 *}
 
 ML{*fun get_thm_alt ctxt (t, n) =
@@ -1672,7 +1671,7 @@
 text {*
   The advantage of @{ML get_thm_alt} is that it leaves very little room for 
   something to go wrong; in contrast it is much more difficult to predict 
-  what happens with @{ML Arith_Data.arith_tac}, especially in more complicated 
+  what happens with @{ML arith_tac in Arith_Data}, especially in more complicated 
   circumstances. The disatvantage of @{ML get_thm_alt} is to find a simpset
   that is sufficiently powerful to solve every instance of the lemmas
   we like to prove. This requires careful tuning, but is often necessary in