--- a/ProgTutorial/Tactical.thy	Tue Mar 31 15:53:12 2009 +0100
+++ b/ProgTutorial/Tactical.thy	Tue Mar 31 16:50:13 2009 +0100
@@ -2107,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