diff -r cecd7a941885 -r 6103b0eadbf2 ProgTutorial/Parsing.thy
--- a/ProgTutorial/Parsing.thy	Tue May 14 17:10:47 2019 +0200
+++ b/ProgTutorial/Parsing.thy	Tue May 14 17:45:13 2019 +0200
@@ -502,11 +502,11 @@
   messages. The following code
 
 
-@{ML_response_fake [display,gray] "Token.explode 
-  (Thy_Header.get_keywords' @{context}) Position.none \"hello world\"" 
-"[Token (\<dots>,(Ident, \"hello\"),\<dots>), 
- Token (\<dots>,(Space, \" \"),\<dots>), 
- Token (\<dots>,(Ident, \"world\"),\<dots>)]"}
+@{ML_response_fake [display,gray] \<open>Token.explode 
+  (Thy_Header.get_keywords' @{context}) Position.none "hello world"\<close>
+\<open>[Token (_,(Ident, "hello"),_), 
+ Token (_,(Space, " "),_), 
+ Token (_,(Ident, "world"),_)]\<close>}
 
   produces three tokens where the first and the last are identifiers, since
   @{text [quotes] "hello"} and @{text [quotes] "world"} do not match any
@@ -526,9 +526,9 @@
 
   @{ML_response_fake [display,gray] "Token.explode 
   (Thy_Header.get_keywords' @{context}) Position.none \"hello world\"" 
-"[Token (\<dots>,(Keyword, \"hello\"),\<dots>), 
- Token (\<dots>,(Space, \" \"),\<dots>), 
- Token (\<dots>,(Ident, \"world\"),\<dots>)]"}
+"[Token (_,(Keyword, \"hello\"),_), 
+ Token (_,(Space, \" \"),_), 
+ Token (_,(Ident, \"world\"),_)]"}
 
   Many parsing functions later on will require white space, comments and the like
   to have already been filtered out.  So from now on we are going to use the 
@@ -541,7 +541,7 @@
 in
    filter Token.is_proper input
 end" 
-"[Token (\<dots>,(Ident, \"hello\"), \<dots>), Token (\<dots>,(Ident, \"world\"), \<dots>)]"}
+"[Token (_,(Ident, \"hello\"), _), Token (_,(Ident, \"world\"), _)]"}
 
   For convenience we define the function:
 \<close>
@@ -555,9 +555,9 @@
 
 @{ML_response_fake [display,gray] 
 "filtered_input \"inductive | for\"" 
-"[Token (\<dots>,(Command, \"inductive\"),\<dots>), 
- Token (\<dots>,(Keyword, \"|\"),\<dots>), 
- Token (\<dots>,(Keyword, \"for\"),\<dots>)]"}
+"[Token (_,(Command, \"inductive\"),_), 
+ Token (_,(Keyword, \"|\"),_), 
+ Token (_,(Keyword, \"for\"),_)]"}
 
   you obtain a list consisting of only one command and two keyword tokens.
   If you want to see which keywords and commands are currently known to Isabelle, 
@@ -575,7 +575,7 @@
 in 
   (Parse.$$$ \"where\" input1, Parse.$$$ \"|\" input2)
 end"
-"((\"where\",\<dots>), (\"|\",\<dots>))"}
+"((\"where\",_), (\"|\",_))"}
 
   Any non-keyword string can be parsed with the function @{ML_ind reserved in Parse}.
   For example:
@@ -609,7 +609,7 @@
 in 
   (Parse.enum \"|\" (Parse.$$$ \"in\")) input
 end" 
-"([\"in\", \"in\", \"in\"], [\<dots>])"}
+"([\"in\", \"in\", \"in\"], [_])"}
 
   The function @{ML_ind enum1 in Parse} works similarly, except that the
   parsed list must be non-empty. Note that we had to add a string @{text
@@ -673,8 +673,8 @@
 
 @{ML_response_fake [display,gray]
 "filtered_input' \"foo \\n bar\""
-"[Token ((\"foo\", ({line=7, end_line=7}, {line=7})), (Ident, \"foo\"), \<dots>),
- Token ((\"bar\", ({line=8, end_line=8}, {line=8})), (Ident, \"bar\"), \<dots>)]"}
+"[Token ((\"foo\", ({line=7, end_line=7}, {line=7})), (Ident, \"foo\"), _),
+ Token ((\"bar\", ({line=8, end_line=8}, {line=8})), (Ident, \"bar\"), _)]"}
 
   in which the @{text [quotes] "\\n"} causes the second token to be in 
   line 8.
@@ -844,9 +844,9 @@
   parse spec_parser input
 end"
 "(([(even, NONE, NoSyn), (odd, NONE, NoSyn)],
-   [((even0,\<dots>),\<dots>),
-    ((evenS,\<dots>),\<dots>),
-    ((oddS,\<dots>),\<dots>)]), [])"}
+   [((even0,_),_),
+    ((evenS,_),_),
+    ((oddS,_),_)]), [])"}
 \<close>
 
 ML \<open>let
@@ -875,8 +875,8 @@
 in
   parse Parse.vars input
 end"
-"([(foo, SOME \<dots>, NoSyn), 
-  (bar, SOME \<dots>, Mixfix (Source {text=\"BAR\",...}, [], 100, \<dots>)), 
+"([(foo, SOME _, NoSyn), 
+  (bar, SOME _, Mixfix (Source {text=\"BAR\",...}, [], 100, _)), 
   (blonk, NONE, NoSyn)],[])"}  
 \<close>
 
@@ -904,7 +904,7 @@
   val ((name, attrib), _) = parse (Parse_Spec.thm_name \":\") input 
 in 
   (name, map Token.name_of_src attrib)
-end" "(foo_lemma, [(\"intro\", \<dots>), (\"dest\", \<dots>)])"}
+end" "(foo_lemma, [(\"intro\", _), (\"dest\", _)])"}
  
   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