--- a/ProgTutorial/Tactical.thy	Mon Mar 30 17:40:20 2009 +0200
+++ b/ProgTutorial/Tactical.thy	Wed Apr 01 12:28:14 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 
@@ -2081,6 +2080,8 @@
 *}
 
 
+section {* Declarations (TBD) *}
+
 section {* Structured Proofs (TBD) *}
 
 text {* TBD *}
@@ -2105,15 +2106,12 @@
   }
 oops
 
-ML {* fun prop ctxt s =
-  Thm.cterm_of (ProofContext.theory_of ctxt) (Syntax.read_prop ctxt s) *}
-
 ML {* 
   val ctxt0 = @{context};
   val ctxt = ctxt0;
   val (_, ctxt) = Variable.add_fixes ["A", "B", "C"] ctxt;
-  val ([r], ctxt) = Assumption.add_assumes [prop ctxt "A & B \<Longrightarrow> C"] ctxt;
-  val (this, ctxt) = Assumption.add_assumes [prop ctxt "A", prop ctxt "B"] ctxt;
+  val ([r], ctxt) = Assumption.add_assumes [@{cprop "A & B \<Longrightarrow> C"}] ctxt
+  val (this, ctxt) = Assumption.add_assumes [@{cprop "A"}, @{cprop "B"}] ctxt;
   val this = [@{thm conjI} OF this]; 
   val this = r OF this;
   val this = Assumption.export false ctxt ctxt0 this