diff -r 82c482467d75 -r c53d74b34123 ProgTutorial/First_Steps.thy
--- a/ProgTutorial/First_Steps.thy	Sun Dec 15 23:49:05 2013 +0000
+++ b/ProgTutorial/First_Steps.thy	Thu Mar 13 17:16:49 2014 +0000
@@ -862,7 +862,7 @@
 
 ML %linenosgray{*val term_pat_setup = 
 let
-  val parser = Args.context -- Scan.lift Args.name_source
+  val parser = Args.context -- Scan.lift Args.name_inner_syntax
 
   fun term_pat (ctxt, str) =
      str |> Proof_Context.read_term_pattern ctxt
@@ -895,7 +895,7 @@
 
 ML %grayML{*val type_pat_setup = 
 let
-  val parser = Args.context -- Scan.lift Args.name_source
+  val parser = Args.context -- Scan.lift Args.name_inner_syntax
 
   fun typ_pat (ctxt, str) =
     let