diff -r 95b42288294e -r 438703674711 ProgTutorial/Advanced.thy
--- a/ProgTutorial/Advanced.thy	Fri May 17 11:21:09 2019 +0200
+++ b/ProgTutorial/Advanced.thy	Tue May 21 14:37:39 2019 +0200
@@ -250,19 +250,19 @@
   of fixed variables is actually quite useful. For example it prevents us from 
   fixing a variable twice
 
-  @{ML_matchresult_fake [gray, display]
+  @{ML_response [gray, display]
   \<open>@{context}
 |> Variable.add_fixes ["x", "x"]\<close> 
-  \<open>ERROR: Duplicate fixed variable(s): "x"\<close>}
+  \<open>Duplicate fixed variable(s): "x"\<close>}
 
   More importantly it also allows us to easily create fresh names for
   fixed variables.  For this you have to use the function @{ML_ind
   variant_fixes in Variable} from the structure @{ML_structure Variable}.
 
-  @{ML_matchresult_fake [gray, display]
+  @{ML_response [gray, display]
   \<open>@{context}
 |> Variable.variant_fixes ["y", "y", "z"]\<close> 
-  \<open>(["y", "ya", "z"], ...)\<close>}
+  \<open>(["y", "ya", "z"],\<dots>\<close>}
 
   Now a fresh variant for the second occurence of \<open>y\<close> is created
   avoiding any clash. In this way we can also create fresh free variables
@@ -271,7 +271,7 @@
   create two fresh variables of type @{typ nat} as variants of the
   string @{text [quotes] "x"} (Lines 6 and 7).
 
-  @{ML_matchresult_fake [display, gray, linenos]
+  @{ML_matchresult [display, gray, linenos]
   \<open>let
   val ctxt0 = @{context}
   val (_, ctxt1) = Variable.add_fixes ["x"] ctxt0
@@ -280,8 +280,8 @@
   (Variable.variant_frees ctxt0 [] frees,
    Variable.variant_frees ctxt1 [] frees)
 end\<close>
-  \<open>([("x", "nat"), ("xa", "nat")], 
- [("xa", "nat"), ("xb", "nat")])\<close>}
+  \<open>([("x", _), ("xa", _)], 
+ [("xa", _), ("xb", _)])\<close>}
 
   As you can see, if we create the fresh variables with the context \<open>ctxt0\<close>,
   then we obtain \<open>x\<close> and \<open>xa\<close>; but in \<open>ctxt1\<close> we obtain \<open>xa\<close>
@@ -291,14 +291,14 @@
   avoiding any variable occurring in those terms. For this you can use the
   function @{ML_ind declare_term in Variable} from the structure @{ML_structure Variable}.
 
-  @{ML_matchresult_fake [gray, display]
+  @{ML_matchresult [gray, display]
   \<open>let
   val ctxt1 = Variable.declare_term @{term "(x, xa)"} @{context}
   val frees = replicate 2 ("x", @{typ nat})
 in
   Variable.variant_frees ctxt1 [] frees
 end\<close>
-  \<open>[("xb", "nat"), ("xc", "nat")]\<close>}
+  \<open>[("xb", _), ("xc", _)]\<close>}
 
   The result is \<open>xb\<close> and \<open>xc\<close> for the names of the fresh
   variables, since \<open>x\<close> and \<open>xa\<close> occur in the term we declared. 
@@ -327,7 +327,7 @@
   the function @{ML_ind read_term in Syntax} from the structure
   @{ML_structure Syntax}. Consider the following code:
 
-  @{ML_matchresult_fake [gray, display]
+  @{ML_response [gray, display]
   \<open>let
   val ctxt0 = @{context}
   val ctxt1 = Variable.declare_term @{term "x::nat"} ctxt0
@@ -343,7 +343,7 @@
   type the parsed term receives depends upon the last declaration that
   is made, as the next example illustrates.
 
-  @{ML_matchresult_fake [gray, display]
+  @{ML_response [gray, display]
   \<open>let
   val ctxt1 = Variable.declare_term @{term "x::nat"} @{context}
   val ctxt2 = Variable.declare_term @{term "x::int"} ctxt1
@@ -398,7 +398,7 @@
   term, in our case @{term "P x y z x y z"}, into a theorem (disregarding 
   whether it is actually provable).
 
-  @{ML_matchresult_fake [display, gray]
+  @{ML_response [display, gray]
   \<open>let
   val thy = @{theory}
   val ctxt0 = @{context}
@@ -416,7 +416,7 @@
   function @{ML_ind export in Assumption} from the structure
   @{ML_structure Assumption}. Consider the following code.
 
-  @{ML_matchresult_fake [display, gray, linenos]
+  @{ML_response [display, gray, linenos]
   \<open>let
   val ctxt0 = @{context}
   val ([eq], ctxt1) = Assumption.add_assumes [@{cprop "x \<equiv> y"}] ctxt0
@@ -448,7 +448,7 @@
   @{ML_structure Variable} and @{ML_structure Assumption}. This can be seen
   in the following example.
 
-  @{ML_matchresult_fake [display, gray]
+  @{ML_response [display, gray]
   \<open>let
   val ctxt0 = @{context}
   val ((fvs, [eq]), ctxt1) = ctxt0
@@ -458,7 +458,7 @@
 in
   Proof_Context.export ctxt1 ctxt0 [eq']
 end\<close>
-  \<open>[?x \<equiv> ?y \<Longrightarrow> ?y \<equiv> ?x]\<close>}
+  \<open>["?x \<equiv> ?y \<Longrightarrow> ?y \<equiv> ?x"]\<close>}
 \<close>