diff -r cecd7a941885 -r 6103b0eadbf2 ProgTutorial/Essential.thy
--- 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