--- a/ProgTutorial/Tactical.thy	Mon Mar 30 17:40:20 2009 +0200
+++ b/ProgTutorial/Tactical.thy	Wed Apr 01 14:50:09 2009 +0200
@@ -2081,6 +2081,8 @@
 *}
 
 
+section {* Declarations (TBD) *}
+
 section {* Structured Proofs (TBD) *}
 
 text {* TBD *}
@@ -2105,15 +2107,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