--- a/ProgTutorial/Essential.thy	Tue May 14 17:10:47 2019 +0200
+++ b/ProgTutorial/Essential.thy	Tue May 14 17:45:13 2019 +0200
@@ -29,8 +29,8 @@
 
   @{ML_response [display,gray] 
 "@{term \"(a::nat) + b = c\"}" 
-"Const (\"HOL.eq\", \<dots>) $ 
-  (Const (\"Groups.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
+"Const (\"HOL.eq\", _) $ 
+  (Const (\"Groups.plus_class.plus\", _) $ _ $ _) $ _"}
 
   constructs the term @{term "(a::nat) + b = c"}. The resulting term is printed using 
   the internal representation corresponding to the datatype @{ML_type_ind "term"}, 
@@ -187,14 +187,14 @@
   Consider for example the pairs
 
 @{ML_response [display,gray] "(@{term \"P x\"}, @{prop \"P x\"})" 
-"(Free (\"P\", \<dots>) $ Free (\"x\", \<dots>),
- Const (\"HOL.Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)))"}
+"(Free (\"P\", _) $ Free (\"x\", _),
+ Const (\"HOL.Trueprop\", _) $ (Free (\"P\", _) $ Free (\"x\", _)))"}
 
   where a coercion is inserted in the second component and 
 
   @{ML_response [display,gray] "(@{term \"P x \<Longrightarrow> Q x\"}, @{prop \"P x \<Longrightarrow> Q x\"})" 
-  "(Const (\"Pure.imp\", \<dots>) $ \<dots> $ \<dots>, 
- Const (\"Pure.imp\", \<dots>) $ \<dots> $ \<dots>)"}
+  "(Const (\"Pure.imp\", _) $ _ $ _, 
+ Const (\"Pure.imp\", _) $ _ $ _)"}
 
   where it is not (since it is already constructed by a meta-implication). 
   The purpose of the \<open>Trueprop\<close>-coercion is to embed formulae of
@@ -202,7 +202,7 @@
   is needed whenever a term is constructed that will be proved as a theorem. 
 
   As already seen above, types can be constructed using the antiquotation 
-  \<open>@{typ \<dots>}\<close>. For example:
+  \<open>@{typ _}\<close>. For example:
 
   @{ML_response_fake [display,gray] "@{typ \"bool \<Rightarrow> nat\"}" "bool \<Rightarrow> nat"}
 
@@ -339,18 +339,18 @@
   the given arguments
 
   @{ML_response [display,gray] "make_imp @{term S} @{term T}" 
-"Const \<dots> $ 
+"Const _ $ 
   Abs (\"x\", Type (\"Nat.nat\",[]),
-    Const \<dots> $ (Free (\"S\",\<dots>) $ \<dots>) $ (Free (\"T\",\<dots>) $ \<dots>))"}
+    Const _ $ (Free (\"S\",_) $ _) $ (Free (\"T\",_) $ _))"}
 
   whereas with @{ML make_wrong_imp} you obtain a term involving the @{term "P"} 
   and \<open>Q\<close> from the antiquotation.
 
   @{ML_response [display,gray] "make_wrong_imp @{term S} @{term T}" 
-"Const \<dots> $ 
-  Abs (\"x\", \<dots>,
-    Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $ 
-                (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"}
+"Const _ $ 
+  Abs (\"x\", _,
+    Const _ $ (Const _ $ (Free (\"P\",_) $ _)) $ 
+                (Const _ $ (Free (\"Q\",_) $ _)))"}
 
   There are a number of handy functions that are frequently used for
   constructing terms. One is the function @{ML_ind list_comb in Term}, which
@@ -449,7 +449,7 @@
   @{ML_response_fake [display, gray]
   "strip_alls @{term \"\<forall>x y. x = (y::bool)\"}"
 "([Free (\"x\", \"bool\"), Free (\"y\", \"bool\")],
-  Const (\"op =\", \<dots>) $ Bound 1 $ Bound 0)"}
+  Const (\"op =\", _) $ Bound 1 $ Bound 0)"}
 
   Note that we produced in the body two dangling de Bruijn indices. 
   Later on we will also use the inverse function that
@@ -605,7 +605,7 @@
   because @{term "All"} is such a fundamental constant, which can be referenced
   by @{ML "Const (\"All\", some_type)" for some_type}. However, if you look at
 
-  @{ML_response [display,gray] "@{term \"Nil\"}" "Const (\"List.list.Nil\", \<dots>)"}
+  @{ML_response [display,gray] "@{term \"Nil\"}" "Const (\"List.list.Nil\", _)"}
 
   the name of the constant \<open>Nil\<close> depends on the theory in which the
   term constructor is defined (\<open>List\<close>) and also in which datatype
@@ -614,8 +614,8 @@
   \mbox{@{term "times"}}:
 
   @{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"times\"})" 
- "(Const (\"Groups.zero_class.zero\", \<dots>), 
- Const (\"Groups.times_class.times\", \<dots>))"}
+ "(Const (\"Groups.zero_class.zero\", _), 
+ Const (\"Groups.times_class.times\", _))"}
 
   While you could use the complete name, for example 
   @{ML "Const (\"List.list.Nil\", some_type)" for some_type}, for referring to or

--- a/ProgTutorial/First_Steps.thy	Tue May 14 17:10:47 2019 +0200
+++ b/ProgTutorial/First_Steps.thy	Tue May 14 17:45:13 2019 +0200
@@ -5,7 +5,6 @@
 chapter \<open>First Steps\label{chp:firststeps}\<close>
 
 
-
 text \<open>
   \begin{flushright}
   {\em ``The most effective debugging tool is still careful thought,\\ 
@@ -104,7 +103,7 @@
   for converting values into strings, namely the antiquotation 
   \<open>@{make_string}\<close>:
 
-  @{ML_response_fake [display,gray] "writeln (@{make_string} 1)" "\"1\""} 
+  @{ML_response_fake [display,gray] \<open>writeln (@{make_string} 1)\<close> \<open>"1"\<close>} 
 
   However, \<open>@{make_string}\<close> only works if the type of what
   is converted is monomorphic and not a function. 

--- a/ProgTutorial/Package/Ind_Interface.thy	Tue May 14 17:10:47 2019 +0200
+++ b/ProgTutorial/Package/Ind_Interface.thy	Tue May 14 17:45:13 2019 +0200
@@ -119,9 +119,9 @@
   parse spec_parser input
 end"
 "(([(even, NONE, NoSyn), (odd, NONE, NoSyn)],
-     [((even0,\<dots>), \<dots>),
-      ((evenS,\<dots>), \<dots>),
-      ((oddS,\<dots>), \<dots>)]), [])"}
+     [((even0,_), _),
+      ((evenS,_), _),
+      ((oddS,_), _)]), [])"}
 
   then we get back the specifications of the predicates (with type and syntax annotations), 
   and specifications of the introduction rules. This is all the information we

--- 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 

--- a/ProgTutorial/Tactical.thy	Tue May 14 17:10:47 2019 +0200
+++ b/ProgTutorial/Tactical.thy	Tue May 14 17:45:13 2019 +0200
@@ -2105,9 +2105,9 @@
 in
   Thm.prop_of (Thm.beta_conversion true ctrm)
 end"
-"Const (\"Pure.eq\",\<dots>) $ 
-  (Abs (\"x\",\<dots>,Abs (\"y\",\<dots>,\<dots>)) $\<dots>$\<dots>) $ 
-    (Const (\"Groups.plus_class.plus\",\<dots>) $ \<dots> $ \<dots>)"} 
+"Const (\"Pure.eq\",_) $ 
+  (Abs (\"x\",_,Abs (\"y\",_,_)) $_$_) $ 
+    (Const (\"Groups.plus_class.plus\",_) $ _ $ _)"} 
 
 or in the pretty-printed form
 

--- a/ProgTutorial/antiquote_setup.ML	Tue May 14 17:10:47 2019 +0200
+++ b/ProgTutorial/antiquote_setup.ML	Tue May 14 17:45:13 2019 +0200
@@ -28,10 +28,11 @@
         |> ml_with_vars vs 
 
 fun ml_pat pat lhs =
-  ML_Lex.read "val " @ ML_Lex.read (translate_string (fn "\<dots>" => "_" | s => s) pat) @ 
+  ML_Lex.read "val " @ ML_Lex.read_source false pat @ 
   ML_Lex.read " = " @
   ML_Lex.read_source false lhs 
 
+
 fun ml_struct src = 
   ML_Lex.read "functor DUMMY_FUNCTOR() = struct structure DUMMY = " @
   ML_Lex.read_source false src @
@@ -89,24 +90,27 @@
 fun output_type ctxt = gen_output_type (K (output ctxt)) ctxt
 fun output_type_ind ctxt = gen_output_type (output_indexed ctxt) ctxt 
 
+val dots_pat = translate_string (fn "_" => "\<dots>"  | s => s) 
+
 (* checks and expression against a result pattern *)
 fun output_response ctxt (lhs, pat) = 
     (eval_fn ctxt (ml_pat pat) lhs;
-     (*eval_fn ctxt (ml_out lhs);*) (*FIXME remove*)
-     output ctxt ((prefix_lines "" (Input.source_content lhs)) @ (prefix_lines "> " pat)))
+     output ctxt ((prefix_lines "" (Input.source_content lhs)) @ 
+       (prefix_lines "> " (dots_pat (Input.source_content pat)))))
 
 (* checks the expressions, but does not check it against a result pattern *)
 fun output_response_fake ctxt (lhs, pat) = 
     (eval_fn ctxt (ml_val [] NONE) lhs;
-     (*eval_fn ctxt (ml_out lhs);*) (* FIXME remove *)
-     output ctxt ((split_lines (Input.source_content lhs)) @ (prefix_lines "> " pat)))
+     output ctxt ( (split_lines (Input.source_content lhs)) @ 
+        (prefix_lines "> " (dots_pat (Input.source_content pat)))))
 
 (* checks the expressions, but does not check it against a result pattern *)
 fun ouput_response_fake_both ctxt (lhs, pat) = 
-    (output ctxt ((split_lines (Input.source_content lhs)) @ (prefix_lines "> " pat)))
+    (output ctxt ((split_lines (Input.source_content lhs)) @ 
+     (prefix_lines "> " (dots_pat (Input.source_content pat)))))
 
 val single_arg = Scan.lift (Args.name)
-val two_args   = Scan.lift (Args.text_input -- Args.name)
+val two_args   = Scan.lift (Args.text_input -- Args.text_input)
 val test = Scan.lift (Args.name -- Args.name -- Scan.option (Args.$$$ "with"  |-- Args.name))
 
 val ml_setup =