--- a/ProgTutorial/Parsing.thy	Sun Dec 15 23:49:05 2013 +0000
+++ b/ProgTutorial/Parsing.thy	Thu Mar 13 17:16:49 2014 +0000
@@ -726,7 +726,7 @@
 (*
 ML {*
 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 |> Syntax.read_prop ctxt
@@ -752,23 +752,19 @@
   for terms and  types: you can just call the predefined parsers. Terms can 
   be parsed using the function @{ML_ind term in Parse}. For example:
 
-@{ML_response [display,gray]
+@{ML_response_fake [display,gray]
 "let 
   val input = Outer_Syntax.scan Position.none \"foo\"
 in 
   Parse.term input
 end"
-"(\"\\^E\\^Ftoken\\^Efoo\\^E\\^F\\^E\", [])"}
+"(\"<markup>\", [])"}
+
 
   The function @{ML_ind prop in Parse} is similar, except that it gives a different
   error message, when parsing fails. As you can see, the parser not just returns 
-  the parsed string, but also some encoded information. You can decode the
-  information with the function @{ML_ind parse in YXML} in @{ML_struct YXML}. For example
-
-  @{ML_response_fake [display,gray]
-  "YXML.parse \"\\^E\\^Ftoken\\^Efoo\\^E\\^F\\^E\""
-  "Text \"\\^E\\^Ftoken\\^Efoo\\^E\\^F\\^E\""}
-
+  the parsed string, but also some markup information. You can decode the
+  information with the function @{ML_ind parse in YXML} in @{ML_struct YXML}. 
   The result of the decoding is an XML-tree. You can see better what is going on if
   you replace @{ML Position.none} by @{ML "Position.line 42"}, say:
 
@@ -847,9 +843,9 @@
   parse spec_parser input
 end"
 "(([(even, NONE, NoSyn), (odd, NONE, NoSyn)],
-     [((even0,\<dots>), \"\\^E\\^Ftoken\\^Eeven 0\\^E\\^F\\^E\"),
-      ((evenS,\<dots>), \"\\^E\\^Ftoken\\^Eodd n \<Longrightarrow> even (Suc n)\\^E\\^F\\^E\"),
-      ((oddS,\<dots>), \"\\^E\\^Ftoken\\^Eeven n \<Longrightarrow> odd (Suc n)\\^E\\^F\\^E\")]), [])"}
+   [((even0,\<dots>),\<dots>),
+    ((evenS,\<dots>),\<dots>),
+    ((oddS,\<dots>),\<dots>)]), [])"}
 
   As you see, the result is a pair consisting of a list of
   variables with optional type-annotation and syntax-annotation, and a list of
@@ -869,8 +865,8 @@
 in
   parse Parse.fixes input
 end"
-"([(foo, SOME \"\\^E\\^Ftoken\\^Eint \<Rightarrow> bool\\^E\\^F\\^E\", NoSyn), 
-  (bar, SOME \"\\^E\\^Ftoken\\^Enat\\^E\\^F\\^E\", Mixfix (\"BAR\", [], 100)), 
+"([(foo, SOME \<dots>, NoSyn), 
+  (bar, SOME \<dots>, Mixfix (\"BAR\", [], 100)), 
   (blonk, NONE, NoSyn)],[])"}  
 *}
 
@@ -897,8 +893,8 @@
   val input = filtered_input \"foo_lemma[intro,dest!]:\"
   val ((name, attrib), _) = parse (Parse_Spec.thm_name \":\") input 
 in 
-  (name, map Args.dest_src attrib)
-end" "(foo_lemma, [((\"intro\", []), \<dots>), ((\"dest\", [\<dots>]), \<dots>)])"}
+  (name, map Args.name_of_src attrib)
+end" "(foo_lemma, [(\"intro\", \<dots>), (\"dest\", \<dots>)])"}
  
   The function @{ML_ind opt_thm_name in Parse_Spec} is the ``optional'' variant of
   @{ML_ind thm_name in Parse_Spec}. Theorem names can contain attributes. The name 
@@ -1133,9 +1129,9 @@
    fun after_qed thm_name thms lthy =
         Local_Theory.note (thm_name, (flat thms)) lthy |> snd
 
-   fun setup_proof (thm_name, (txt, pos)) lthy =
+   fun setup_proof (thm_name, {text, ...}) lthy =
      let
-       val trm = Code_Runtime.value lthy result_cookie ("", txt)
+       val trm = Code_Runtime.value lthy result_cookie ("", text)
      in
        Proof.theorem NONE (after_qed thm_name) [[(trm, [])]] lthy
      end