--- a/ProgTutorial/First_Steps.thy	Sat Nov 12 11:45:39 2011 +0000
+++ b/ProgTutorial/First_Steps.thy	Thu Nov 24 19:54:01 2011 +0000
@@ -938,9 +938,13 @@
   val parser = Args.context -- Scan.lift Args.name_source
 
   fun typ_pat (ctxt, str) =
-     str |> Syntax.parse_typ ctxt
-         |> ML_Syntax.print_typ
-         |> ML_Syntax.atomic
+    let
+      val ctxt' = Proof_Context.set_mode Proof_Context.mode_schematic ctxt
+    in 
+      str |> Syntax.read_typ ctxt'
+          |> ML_Syntax.print_typ
+          |> ML_Syntax.atomic
+      end
 in
   ML_Antiquote.inline @{binding "typ_pat"} (parser >> typ_pat)
 end*}