
diff -r 6103b0eadbf2 -r f7c97e64cc2a ProgTutorial/Essential.thy
--- a/ProgTutorial/Essential.thy	Tue May 14 17:45:13 2019 +0200
+++ b/ProgTutorial/Essential.thy	Thu May 16 19:56:12 2019 +0200
@@ -27,7 +27,7 @@
   Uncertified terms are often just called terms. One way to construct them is by 
   using the antiquotation \mbox{\<open>@{term \<dots>}\<close>}. For example
 
-  @{ML_response [display,gray] 
+  @{ML_matchresult [display,gray] 
 "@{term \"(a::nat) + b = c\"}" 
 "Const (\"HOL.eq\", _) $ 
   (Const (\"Groups.plus_class.plus\", _) $ _ $ _) $ _"}
@@ -53,7 +53,7 @@
   terms use the usual de Bruijn index mechanism for representing bound
   variables.  For example in
 
-  @{ML_response_fake [display, gray]
+  @{ML_matchresult_fake [display, gray]
   "@{term \"\<lambda>x y. x y\"}"
   "Abs (\"x\", \"'a \<Rightarrow> 'b\", Abs (\"y\", \"'a\", Bound 1 $ Bound 0))"}
 
@@ -69,7 +69,7 @@
   Be careful if you pretty-print terms. Consider pretty-printing the abstraction
   term shown above:
 
-  @{ML_response_fake [display, gray]
+  @{ML_matchresult_fake [display, gray]
 "@{term \"\<lambda>x y. x y\"}
   |> pretty_term @{context}
   |> pwriteln"
@@ -79,7 +79,7 @@
   tacitly eta-contracted the output. You obtain a similar result 
   with beta-redexes
 
-  @{ML_response_fake [display, gray]
+  @{ML_matchresult_fake [display, gray]
 "let 
   val redex = @{term \"(\<lambda>(x::int) (y::int). x)\"} 
   val arg1 = @{term \"1::int\"} 
@@ -97,7 +97,7 @@
   value @{ML_ind show_abbrevs in Syntax}. For example
 
 
-  @{ML_response_fake [display, gray]
+  @{ML_matchresult_fake [display, gray]
   "let 
   val redex = @{term \"(\<lambda>(x::int) (y::int). x)\"} 
   val arg1 = @{term \"1::int\"} 
@@ -114,7 +114,7 @@
   \emph{schematic} variables (term-constructor @{ML Var} and written with a
   leading question mark). Consider the following two examples
   
-  @{ML_response_fake [display, gray]
+  @{ML_matchresult_fake [display, gray]
 "let
   val v1 = Var ((\"x\", 3), @{typ bool})
   val v2 = Var ((\"x1\", 3), @{typ bool})
@@ -144,14 +144,14 @@
   Constructing terms via antiquotations has the advantage that only typable
   terms can be constructed. For example
 
-  @{ML_response_fake_both [display,gray]
+  @{ML_matchresult_fake_both [display,gray]
   "@{term \"x x\"}"
   "Type unification failed: Occurs check!"}
 
   raises a typing error, while it is perfectly ok to construct the term
   with the raw ML-constructors:
 
-  @{ML_response_fake [display,gray] 
+  @{ML_matchresult_fake [display,gray] 
 "let
   val omega = Free (\"x\", @{typ \"nat \<Rightarrow> nat\"}) $ Free (\"x\", @{typ nat})
 in 
@@ -186,13 +186,13 @@
   usually invisible \<open>Trueprop\<close>-coercions whenever necessary. 
   Consider for example the pairs
 
-@{ML_response [display,gray] "(@{term \"P x\"}, @{prop \"P x\"})" 
+@{ML_matchresult [display,gray] "(@{term \"P x\"}, @{prop \"P x\"})" 
 "(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\"})" 
+  @{ML_matchresult [display,gray] "(@{term \"P x \<Longrightarrow> Q x\"}, @{prop \"P x \<Longrightarrow> Q x\"})" 
   "(Const (\"Pure.imp\", _) $ _ $ _, 
  Const (\"Pure.imp\", _) $ _ $ _)"}
 
@@ -204,7 +204,7 @@
   As already seen above, types can be constructed using the antiquotation 
   \<open>@{typ _}\<close>. For example:
 
-  @{ML_response_fake [display,gray] "@{typ \"bool \<Rightarrow> nat\"}" "bool \<Rightarrow> nat"}
+  @{ML_matchresult_fake [display,gray] "@{typ \"bool \<Rightarrow> nat\"}" "bool \<Rightarrow> nat"}
 
   The corresponding datatype is
 \<close>
@@ -224,7 +224,7 @@
   example, because Isabelle always pretty prints types (unlike terms).
   Using just the antiquotation \<open>@{typ "bool"}\<close> we only see
 
-  @{ML_response [display, gray]
+  @{ML_matchresult [display, gray]
   "@{typ \"bool\"}"
   "bool"}
   which is the pretty printed version of \<open>bool\<close>. However, in PolyML
@@ -263,13 +263,13 @@
 text \<open>
   Now the type bool is printed out in full detail.
 
-  @{ML_response [display,gray]
+  @{ML_matchresult [display,gray]
   "@{typ \"bool\"}"
   "Type (\"HOL.bool\", [])"}
 
   When printing out a list-type
   
-  @{ML_response [display,gray]
+  @{ML_matchresult [display,gray]
   "@{typ \"'a list\"}"
   "Type (\"List.list\", [TFree (\"'a\", [\"HOL.type\"])])"}
 
@@ -279,7 +279,7 @@
   \<open>fun\<close> is defined in the theory \<open>HOL\<close>, it is  
   still represented by its simple name.
 
-   @{ML_response [display,gray]
+   @{ML_matchresult [display,gray]
   "@{typ \"bool \<Rightarrow> nat\"}"
   "Type (\"fun\", [Type (\"HOL.bool\", []), Type (\"Nat.nat\", [])])"}
 
@@ -294,7 +294,7 @@
   After that the types for booleans, lists and so on are printed out again 
   the standard Isabelle way.
 
-  @{ML_response_fake [display, gray]
+  @{ML_matchresult_fake [display, gray]
   "@{typ \"bool\"};
 @{typ \"'a list\"}"
   "\"bool\"
@@ -338,7 +338,7 @@
   to both functions. With @{ML make_imp} you obtain the intended term involving 
   the given arguments
 
-  @{ML_response [display,gray] "make_imp @{term S} @{term T}" 
+  @{ML_matchresult [display,gray] "make_imp @{term S} @{term T}" 
 "Const _ $ 
   Abs (\"x\", Type (\"Nat.nat\",[]),
     Const _ $ (Free (\"S\",_) $ _) $ (Free (\"T\",_) $ _))"}
@@ -346,7 +346,7 @@
   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}" 
+  @{ML_matchresult [display,gray] "make_wrong_imp @{term S} @{term T}" 
 "Const _ $ 
   Abs (\"x\", _,
     Const _ $ (Const _ $ (Free (\"P\",_) $ _)) $ 
@@ -358,7 +358,7 @@
   term list applied to the term. For example
 
 
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "let
   val trm = @{term \"P::bool \<Rightarrow> bool \<Rightarrow> bool\"}
   val args = [@{term \"True\"}, @{term \"False\"}]
@@ -371,7 +371,7 @@
   Another handy function is @{ML_ind lambda in Term}, which abstracts a variable 
   in a term. For example
 
-  @{ML_response_fake [display,gray]
+  @{ML_matchresult_fake [display,gray]
 "let
   val x_nat = @{term \"x::nat\"}
   val trm = @{term \"(P::nat \<Rightarrow> bool) x\"}
@@ -387,7 +387,7 @@
   is of the same type as the abstracted variable. If it is of different type,
   as in
 
-  @{ML_response_fake [display,gray]
+  @{ML_matchresult_fake [display,gray]
 "let
   val x_int = @{term \"x::int\"}
   val trm = @{term \"(P::nat \<Rightarrow> bool) x\"}
@@ -406,7 +406,7 @@
   "(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0 x"} the subterm @{term "(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0"} by
   @{term y}, and @{term x} by @{term True}.
 
-  @{ML_response_fake [display,gray]
+  @{ML_matchresult_fake [display,gray]
 "let
   val sub1 = (@{term \"(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0\"}, @{term \"y::nat \<Rightarrow> nat\"})
   val sub2 = (@{term \"x::nat\"}, @{term \"True\"})
@@ -419,7 +419,7 @@
   As can be seen, @{ML subst_free} does not take typability into account.
   However it takes alpha-equivalence into account:
 
-  @{ML_response_fake [display, gray]
+  @{ML_matchresult_fake [display, gray]
 "let
   val sub = (@{term \"(\<lambda>y::nat. y)\"}, @{term \"x::nat\"})
   val trm = @{term \"(\<lambda>x::nat. x)\"}
@@ -446,7 +446,7 @@
   The function returns a pair consisting of the stripped off variables and
   the body of the universal quantification. For example
 
-  @{ML_response_fake [display, gray]
+  @{ML_matchresult_fake [display, gray]
   "strip_alls @{term \"\<forall>x y. x = (y::bool)\"}"
 "([Free (\"x\", \"bool\"), Free (\"y\", \"bool\")],
   Const (\"op =\", _) $ Bound 1 $ Bound 0)"}
@@ -466,7 +466,7 @@
   bound variables. With the function @{ML subst_bounds}, you can replace these
   loose @{ML_ind Bound in Term}s with the stripped off variables.
 
-  @{ML_response_fake [display, gray, linenos]
+  @{ML_matchresult_fake [display, gray, linenos]
   "let
   val (vrs, trm) = strip_alls @{term \"\<forall>x y. x = (y::bool)\"}
 in 
@@ -488,7 +488,7 @@
   the loose de Bruijn index is replaced by a unique free variable. For example
 
 
-  @{ML_response_fake [display,gray]
+  @{ML_matchresult_fake [display,gray]
   "let
   val body = Bound 0 $ Free (\"x\", @{typ nat})
 in
@@ -501,7 +501,7 @@
   @{ML_ind incr_boundvars in Term}, increases by an integer the indices 
   of the loose bound variables in a term. In the code below
 
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "@{term \"\<forall>x y z u. z = u\"}
   |> strip_alls
   ||> incr_boundvars 2
@@ -519,7 +519,7 @@
   The second function, @{ML_ind loose_bvar1 in Text}, tests whether a term
   contains a loose bound of a certain index. For example
 
-  @{ML_response_fake [gray,display]
+  @{ML_matchresult_fake [gray,display]
 "let
   val body = snd (strip_alls @{term \"\<forall>x y. x = (y::bool)\"})
 in
@@ -530,11 +530,11 @@
   "[true, true, false]"}
 
   There are also many convenient functions that construct specific HOL-terms
-  in the structure @{ML_struct HOLogic}. For example @{ML_ind mk_eq in
+  in the structure @{ML_structure HOLogic}. For example @{ML_ind mk_eq in
   HOLogic} constructs an equality out of two terms.  The types needed in this
   equality are calculated from the type of the arguments. For example
 
-@{ML_response_fake [gray,display]
+@{ML_matchresult_fake [gray,display]
 "let
   val eq = HOLogic.mk_eq (@{term \"True\"}, @{term \"False\"})
 in
@@ -569,7 +569,7 @@
 text \<open>
   will not correctly match the formula @{prop[source] "\<forall>x::nat. P x"}: 
 
-  @{ML_response [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "false"}
+  @{ML_matchresult [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "false"}
 
   The problem is that the \<open>@term\<close>-antiquotation in the pattern 
   fixes the type of the constant @{term "All"} to be @{typ "('a \<Rightarrow> bool) \<Rightarrow> bool"} for 
@@ -583,7 +583,7 @@
 text \<open>
   because now
 
-  @{ML_response [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "true"}
+  @{ML_matchresult [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "true"}
 
   matches correctly (the first wildcard in the pattern matches any type and the
   second any term).
@@ -598,14 +598,14 @@
 text \<open>
   Unfortunately, also this function does \emph{not} work as expected, since
 
-  @{ML_response [display,gray] "is_nil @{term \"Nil\"}" "false"}
+  @{ML_matchresult [display,gray] "is_nil @{term \"Nil\"}" "false"}
 
   The problem is that on the ML-level the name of a constant is more
   subtle than you might expect. The function @{ML is_all} worked correctly,
   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\", _)"}
+  @{ML_matchresult [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
@@ -613,7 +613,7 @@
   type-classes. Consider for example the constants for @{term "zero"} and
   \mbox{@{term "times"}}:
 
-  @{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"times\"})" 
+  @{ML_matchresult [display,gray] "(@{term \"0::nat\"}, @{term \"times\"})" 
  "(Const (\"Groups.zero_class.zero\", _), 
  Const (\"Groups.times_class.times\", _))"}
 
@@ -636,7 +636,7 @@
   The antiquotation for properly referencing type constants is \<open>@{type_name \<dots>}\<close>.
   For example
 
-  @{ML_response [display,gray]
+  @{ML_matchresult [display,gray]
   "@{type_name \"list\"}" "\"List.list\""}
 
   Although types of terms can often be inferred, there are many
@@ -674,7 +674,7 @@
 text \<open>
   Here is an example:
 
-@{ML_response_fake [display,gray] 
+@{ML_matchresult_fake [display,gray] 
 "map_types nat_to_int @{term \"a = (1::nat)\"}" 
 "Const (\"op =\", \"int \<Rightarrow> int \<Rightarrow> bool\")
            $ Free (\"a\", \"int\") $ Const (\"HOL.one_class.one\", \"int\")"}
@@ -691,7 +691,7 @@
   So in order to obtain the list of type-variables of a term you have to 
   call them as follows
 
-  @{ML_response [gray,display]
+  @{ML_matchresult [gray,display]
   "Term.add_tfrees @{term \"(a, b)\"} []"
   "[(\"'b\", [\"HOL.type\"]), (\"'a\", [\"HOL.type\"])]"}
 
@@ -776,7 +776,7 @@
   Let us begin with describing the unification and matching functions for
   types.  Both return type environments (ML-type @{ML_type "Type.tyenv"})
   which map schematic type variables to types and sorts. Below we use the
-  function @{ML_ind typ_unify in Sign} from the structure @{ML_struct Sign}
+  function @{ML_ind typ_unify in Sign} from the structure @{ML_structure Sign}
   for unifying the types \<open>?'a * ?'b\<close> and \<open>?'b list *
   nat\<close>. This will produce the mapping, or type environment, \<open>[?'a :=
   ?'b list, ?'b := nat]\<close>.
@@ -796,9 +796,9 @@
   below. In case of failure, @{ML typ_unify in Sign} will raise the exception
   \<open>TUNIFY\<close>.  We can print out the resulting type environment bound to 
   @{ML tyenv_unif} with the built-in function @{ML_ind dest in Vartab} from the
-  structure @{ML_struct Vartab}.
-
-  @{ML_response_fake [display,gray]
+  structure @{ML_structure Vartab}.
+
+  @{ML_matchresult_fake [display,gray]
   "Vartab.dest tyenv_unif"
   "[((\"'a\", 0), ([\"HOL.type\"], \"?'b List.list\")), 
  ((\"'b\", 0), ([\"HOL.type\"], \"nat\"))]"} 
@@ -839,7 +839,7 @@
   environment in the example this function prints out the more legible:
 
 
-  @{ML_response_fake [display, gray]
+  @{ML_matchresult_fake [display, gray]
   "pretty_tyenv @{context} tyenv_unif"
   "[?'a := ?'b list, ?'b := nat]"}
 
@@ -882,7 +882,7 @@
   of sort information by setting @{ML_ind show_sorts in Syntax} to 
   true. This allows us to inspect the typing environment.
 
-  @{ML_response_fake [display,gray]
+  @{ML_matchresult_fake [display,gray]
   "pretty_tyenv @{context} tyenv"
   "[?'a::s1 := ?'a1::{s1, s2}, ?'b::s2 := ?'a1::{s1, s2}]"}
 
@@ -891,7 +891,7 @@
   type variable has been introduced the @{ML index}, originally being \<open>0\<close>, 
   has been increased to \<open>1\<close>.
 
-  @{ML_response [display,gray]
+  @{ML_matchresult [display,gray]
   "index"
   "1"}
 
@@ -899,7 +899,7 @@
   \<open>?'b list * nat\<close> from the beginning of this section, and the 
   calculated type environment @{ML tyenv_unif}:
 
-  @{ML_response_fake [display, gray]
+  @{ML_matchresult_fake [display, gray]
   "pretty_tyenv @{context} tyenv_unif"
   "[?'a := ?'b list, ?'b := nat]"}
 
@@ -911,12 +911,12 @@
   performance reasons. To apply such a type environment to a type, say \<open>?'a *
   ?'b\<close>, you should use the function @{ML_ind norm_type in Envir}:
 
-  @{ML_response_fake [display, gray]
+  @{ML_matchresult_fake [display, gray]
   "Envir.norm_type tyenv_unif @{typ_pat \"?'a * ?'b\"}"
   "nat list * nat"}
 
   Matching of types can be done with the function @{ML_ind typ_match in Sign}
-  also from the structure @{ML_struct Sign}. This function returns a @{ML_type
+  also from the structure @{ML_structure Sign}. This function returns a @{ML_type
   Type.tyenv} as well, but might raise the exception \<open>TYPE_MATCH\<close> in case
   of failure. For example
 \<close>
@@ -931,7 +931,7 @@
 text \<open>
   Printing out the calculated matcher gives
 
-  @{ML_response_fake [display,gray]
+  @{ML_matchresult_fake [display,gray]
   "pretty_tyenv @{context} tyenv_match"
   "[?'a := bool list, ?'b := nat]"}
   
@@ -939,7 +939,7 @@
   applying the matcher to a type needs to be done with the function
   @{ML_ind subst_type in Envir}. For example
 
-  @{ML_response_fake [display, gray]
+  @{ML_matchresult_fake [display, gray]
   "Envir.subst_type tyenv_match @{typ_pat \"?'a * ?'b\"}"
   "bool list * nat"}
 
@@ -960,14 +960,14 @@
   Now @{ML tyenv_unif} is equal to @{ML tyenv_match'}. If we apply 
   @{ML norm_type in Envir} to the type \<open>?'a * ?'b\<close> we obtain
 
-  @{ML_response_fake [display, gray]
+  @{ML_matchresult_fake [display, gray]
   "Envir.norm_type tyenv_match' @{typ_pat \"?'a * ?'b\"}"
   "nat list * nat"}
 
   which does not solve the matching problem, and if
   we apply @{ML subst_type in Envir} to the same type we obtain
 
-  @{ML_response_fake [display, gray]
+  @{ML_matchresult_fake [display, gray]
   "Envir.subst_type tyenv_unif @{typ_pat \"?'a * ?'b\"}"
   "?'b list * nat"}
   
@@ -1023,7 +1023,7 @@
   the type environment is empty and can be ignored. The 
   resulting term environment is
 
-  @{ML_response_fake [display, gray]
+  @{ML_matchresult_fake [display, gray]
   "pretty_env @{context} fo_env"
   "[?X := P, ?Y := \<lambda>a b. Q b a]"}
 
@@ -1033,7 +1033,7 @@
   unifiers). The function @{ML subst_term in Envir} expects a type environment,
   which is set to empty in the example below, and a term environment.
 
-  @{ML_response_fake [display, gray]
+  @{ML_matchresult_fake [display, gray]
   "let
   val trm = @{term_pat \"(?X::(nat\<Rightarrow>nat\<Rightarrow>nat)\<Rightarrow>bool) ?Y\"}
 in
@@ -1050,7 +1050,7 @@
   matching \<open>\<lambda>x. P x\<close> against the pattern \<open>\<lambda>y. ?X y\<close>. In this
   case, first-order matching produces \<open>[?X := P]\<close>.
 
-  @{ML_response_fake [display, gray]
+  @{ML_matchresult_fake [display, gray]
   "let
   val fo_pat = @{term_pat \"\<lambda>y. (?X::nat\<Rightarrow>bool) y\"}
   val trm = @{term \"\<lambda>x. (P::nat\<Rightarrow>bool) x\"} 
@@ -1071,11 +1071,11 @@
   In particular this excludes terms where a
   schematic variable is an argument of another one and where a schematic
   variable is applied twice with the same bound variable. The function
-  @{ML_ind pattern in Pattern} in the structure @{ML_struct Pattern} tests
+  @{ML_ind pattern in Pattern} in the structure @{ML_structure Pattern} tests
   whether a term satisfies these restrictions under the assumptions
   that it is beta-normal, well-typed and has no loose bound variables.
 
-  @{ML_response [display, gray]
+  @{ML_matchresult [display, gray]
   "let
   val trm_list = 
         [@{term_pat \"?X\"}, @{term_pat \"a\"},
@@ -1099,9 +1099,9 @@
   record of type @{ML_type Envir.env} containing a max-index, a type environment 
   and a term environment). The corresponding functions are @{ML_ind match in Pattern}
   and @{ML_ind unify in Pattern}, both implemented in the structure
-  @{ML_struct Pattern}. An example for higher-order pattern unification is
-
-  @{ML_response_fake [display, gray]
+  @{ML_structure Pattern}. An example for higher-order pattern unification is
+
+  @{ML_matchresult_fake [display, gray]
   "let
   val trm1 = @{term_pat \"\<lambda>x y. g (?X y x) (f (?Y x))\"}
   val trm2 = @{term_pat \"\<lambda>u v. g u (f u)\"}
@@ -1152,7 +1152,7 @@
 
   We can print them out as follows.
 
-  @{ML_response_fake [display, gray]
+  @{ML_matchresult_fake [display, gray]
   "pretty_env @{context} (Envir.term_env un1);
 pretty_env @{context} (Envir.term_env un2);
 pretty_env @{context} (Envir.term_env un3)"
@@ -1164,7 +1164,7 @@
   In case of failure the function @{ML_ind unifiers in Unify} does not raise
   an exception, rather returns the empty sequence. For example
 
-  @{ML_response [display, gray]
+  @{ML_matchresult [display, gray]
 "let 
   val trm1 = @{term \"a\"}
   val trm2 = @{term \"b\"}
@@ -1181,7 +1181,7 @@
   called. This function has a built-in bound, which can be accessed and
   manipulated as a configuration value. For example
 
-  @{ML_response_fake [display,gray]
+  @{ML_matchresult_fake [display,gray]
   "Config.get_global @{theory} (Unify.search_bound)"
   "Int 60"}
 
@@ -1192,7 +1192,7 @@
 
 
   For higher-order matching the function is called @{ML_ind matchers in Unify}
-  implemented in the structure @{ML_struct Unify}. Also this function returns
+  implemented in the structure @{ML_structure Unify}. Also this function returns
   sequences with possibly more than one matcher.  Like @{ML unifiers in
   Unify}, this function does not raise an exception in case of failure, but
   returns an empty sequence. It also first tries out whether the matching
@@ -1213,7 +1213,7 @@
   this problem is to instantiate the schematic variables \<open>?P\<close> and
   \<open>?x\<close>.  Instantiation function for theorems is 
   @{ML_ind instantiate_normalize in Drule} from the structure 
-  @{ML_struct Drule}. One problem, however, is
+  @{ML_structure Drule}. One problem, however, is
   that this function expects the instantiations as lists of @{ML_type "((indexname * sort) * ctyp)"}
   respective @{ML_type "(indexname * typ) * cterm"}:
 
@@ -1266,7 +1266,7 @@
   @{term "Q True"}. 
  
 
-  @{ML_response_fake [gray,display,linenos] 
+  @{ML_matchresult_fake [gray,display,linenos] 
   "let  
   val pat = Logic.strip_imp_concl (Thm.prop_of @{thm spec})
   val trm = @{term \"Trueprop (Q True)\"}
@@ -1354,14 +1354,14 @@
   Given a well-typed term, the function @{ML_ind type_of in Term} returns the 
   type of a term. Consider for example:
 
-  @{ML_response [display,gray] 
+  @{ML_matchresult [display,gray] 
   "type_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::nat\"})" "bool"}
 
   To calculate the type, this function traverses the whole term and will
   detect any typing inconsistency. For example changing the type of the variable 
   @{term "x"} from @{typ "nat"} to @{typ "int"} will result in the error message: 
 
-  @{ML_response_fake [display,gray] 
+  @{ML_matchresult_fake [display,gray] 
   "type_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::int\"})" 
   "*** Exception- TYPE (\"type_of: type mismatch in application\" \<dots>"}
 
@@ -1369,13 +1369,13 @@
   not necessary, there is the function @{ML_ind fastype_of in Term}, which 
   also returns the type of a term.
 
-  @{ML_response [display,gray] 
+  @{ML_matchresult [display,gray] 
   "fastype_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::nat\"})" "bool"}
 
   However, efficiency is gained on the expense of skipping some tests. You 
   can see this in the following example
 
-   @{ML_response [display,gray] 
+   @{ML_matchresult [display,gray] 
   "fastype_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::int\"})" "bool"}
 
   where no error is detected.
@@ -1387,7 +1387,7 @@
   complete type. The type inference can be invoked with the function
   @{ML_ind check_term in Syntax}. An example is as follows:
 
-  @{ML_response_fake [display,gray] 
+  @{ML_matchresult_fake [display,gray] 
 "let
   val c = Const (@{const_name \"plus\"}, dummyT) 
   val o = @{term \"1::nat\"} 
@@ -1432,26 +1432,26 @@
   Certification is always relative to a context. For example you can 
   write:
 
-  @{ML_response_fake [display,gray] 
+  @{ML_matchresult_fake [display,gray] 
   "Thm.cterm_of @{context} @{term \"(a::nat) + b = c\"}" 
   "a + b = c"}
 
   This can also be written with an antiquotation:
 
-  @{ML_response_fake [display,gray] 
+  @{ML_matchresult_fake [display,gray] 
   "@{cterm \"(a::nat) + b = c\"}" 
   "a + b = c"}
 
   Attempting to obtain the certified term for
 
-  @{ML_response_fake_both [display,gray] 
+  @{ML_matchresult_fake_both [display,gray] 
   "@{cterm \"1 + True\"}" 
   "Type unification failed \<dots>"}
 
   yields an error (since the term is not typable). A slightly more elaborate
   example that type-checks is:
 
-@{ML_response_fake [display,gray] 
+@{ML_matchresult_fake [display,gray] 
 "let
   val natT = @{typ \"nat\"}
   val zero = @{term \"0::nat\"}
@@ -1465,13 +1465,13 @@
   you obtain the certified type for the Isabelle type @{typ "nat \<Rightarrow> bool"} on 
   the ML-level as follows:
 
-  @{ML_response_fake [display,gray]
+  @{ML_matchresult_fake [display,gray]
   "Thm.ctyp_of @{context} (@{typ nat} --> @{typ bool})"
   "nat \<Rightarrow> bool"}
 
   or with the antiquotation:
 
-  @{ML_response_fake [display,gray]
+  @{ML_matchresult_fake [display,gray]
   "@{ctyp \"nat \<Rightarrow> bool\"}"
   "nat \<Rightarrow> bool"}
 
@@ -1479,14 +1479,14 @@
   pattern-match against them. However, we can construct them. For example
   the function @{ML_ind apply in Thm} produces a certified application.
 
-  @{ML_response_fake [display,gray]
+  @{ML_matchresult_fake [display,gray]
   "Thm.apply @{cterm \"P::nat \<Rightarrow> bool\"} @{cterm \"3::nat\"}"
   "P 3"}
 
-  Similarly the function @{ML_ind list_comb in Drule} from the structure @{ML_struct Drule}
+  Similarly the function @{ML_ind list_comb in Drule} from the structure @{ML_structure Drule}
   applies a list of @{ML_type cterm}s.
 
-  @{ML_response_fake [display,gray]
+  @{ML_matchresult_fake [display,gray]
   "let
   val chead = @{cterm \"P::unit \<Rightarrow> nat \<Rightarrow> bool\"}
   val cargs = [@{cterm \"()\"}, @{cterm \"3::nat\"}]
@@ -1546,7 +1546,7 @@
   If we print out the value of @{ML my_thm} then we see only the 
   final statement of the theorem.
 
-  @{ML_response_fake [display, gray]
+  @{ML_matchresult_fake [display, gray]
   "pwriteln (pretty_thm @{context} my_thm)"
   "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}
 
@@ -1570,7 +1570,7 @@
   yet stored in Isabelle's theorem database. Consequently, it cannot be 
   referenced on the user level. One way to store it in the theorem database is
   by using the function @{ML_ind note in Local_Theory} from the structure 
-  @{ML_struct Local_Theory} (the Isabelle command
+  @{ML_structure Local_Theory} (the Isabelle command
   \isacommand{local\_setup} will be explained in more detail in 
   Section~\ref{sec:local}).
 \<close>
@@ -1606,13 +1606,13 @@
   Note that we have to use another name under which the theorem is stored,
   since Isabelle does not allow us to call  @{ML_ind note in Local_Theory} twice
   with the same name. The attribute needs to be wrapped inside the function @{ML_ind
-  internal in Attrib} from the structure @{ML_struct Attrib}. If we use the function 
+  internal in Attrib} from the structure @{ML_structure Attrib}. If we use the function 
   @{ML get_thm_names_from_ss} from
   the previous chapter, we can check whether the theorem has actually been
   added.
 
 
-  @{ML_response [display,gray]
+  @{ML_matchresult [display,gray]
   "let
   fun pred s = match_string \"my_thm_simp\" s
 in
@@ -1716,7 +1716,7 @@
 text \<open>
   Testing them for alpha equality produces:
 
-  @{ML_response [display,gray]
+  @{ML_matchresult [display,gray]
 "(Thm.eq_thm_prop (@{thm thm1}, @{thm thm2}),
  Thm.eq_thm_prop (@{thm thm2}, @{thm thm3}))"
 "(true, false)"}
@@ -1725,7 +1725,7 @@
   the functions @{ML_ind lhs_of in Thm} and @{ML_ind rhs_of in Thm} return 
   the left and right-hand side, respectively, of a meta-equality.
 
-  @{ML_response_fake [display,gray]
+  @{ML_matchresult_fake [display,gray]
   "let
   val eq = @{thm True_def}
 in
@@ -1745,7 +1745,7 @@
 text \<open>
   We can destruct them into premises and conclusions as follows. 
 
- @{ML_response_fake [display,gray]
+ @{ML_matchresult_fake [display,gray]
 "let
   val ctxt = @{context}
   fun prems_and_concl thm =
@@ -1778,7 +1778,7 @@
   this, we build the theorem @{term "True \<equiv> True"} (Line 1) and then 
   unfold the constant @{term "True"} according to its definition (Line 2).
 
-  @{ML_response_fake [display,gray,linenos]
+  @{ML_matchresult_fake [display,gray,linenos]
   "Thm.reflexive @{cterm \"True\"}
   |> Simplifier.rewrite_rule @{context} [@{thm True_def}]
   |> pretty_thm @{context}
@@ -1795,14 +1795,14 @@
   @{ML_ind rulify in Object_Logic} 
   replaces all object connectives by equivalents in the meta logic. For example
 
-  @{ML_response_fake [display, gray]
+  @{ML_matchresult_fake [display, gray]
   "Object_Logic.rulify @{context} @{thm foo_test2}"
   "\<lbrakk>?A; ?B\<rbrakk> \<Longrightarrow> ?C"}
 
   The transformation in the other direction can be achieved with function
   @{ML_ind atomize in Object_Logic} and the following code.
 
-  @{ML_response_fake [display,gray]
+  @{ML_matchresult_fake [display,gray]
   "let
   val thm = @{thm foo_test1}
   val meta_eq = Object_Logic.atomize @{context} (Thm.cprop_of thm)
@@ -1837,16 +1837,16 @@
 text \<open>
   This function produces for the theorem @{thm [source] list.induct}
 
-  @{ML_response_fake [display, gray]
+  @{ML_matchresult_fake [display, gray]
   "atomize_thm @{context} @{thm list.induct}"
   "\<forall>P list. P [] \<longrightarrow> (\<forall>a list. P list \<longrightarrow> P (a # list)) \<longrightarrow> P list"}
 
   Theorems can also be produced from terms by giving an explicit proof. 
   One way to achieve this is by using the function @{ML_ind prove in Goal}
-  in the structure @{ML_struct Goal}. For example below we use this function
+  in the structure @{ML_structure Goal}. For example below we use this function
   to prove the term @{term "P \<Longrightarrow> P"}.
   
-  @{ML_response_fake [display,gray]
+  @{ML_matchresult_fake [display,gray]
   "let
   val trm = @{term \"P \<Longrightarrow> P::bool\"}
   val tac = K (assume_tac @{context} 1)
@@ -1878,7 +1878,7 @@
   With them we can now produce three theorem instances of the 
   proposition.
 
-  @{ML_response_fake [display, gray]
+  @{ML_matchresult_fake [display, gray]
   "multi_test @{context} 3"
   "[\"?f ?x = ?f ?x\", \"?f ?x = ?f ?x\", \"?f ?x = ?f ?x\"]"}
 
@@ -1898,12 +1898,12 @@
 text \<open>
   While the LCF-approach of going through interfaces ensures soundness in Isabelle, there
   is the function @{ML_ind make_thm in Skip_Proof} in the structure 
-  @{ML_struct Skip_Proof} that allows us to turn any proposition into a theorem.
+  @{ML_structure Skip_Proof} that allows us to turn any proposition into a theorem.
   Potentially making the system unsound.  This is sometimes useful for developing 
   purposes, or when explicit proof construction should be omitted due to performace 
   reasons. An example of this function is as follows:
 
-  @{ML_response_fake [display, gray]
+  @{ML_matchresult_fake [display, gray]
   "Skip_Proof.make_thm @{theory} @{prop \"True = False\"}"
   "True = False"}
 
@@ -1926,14 +1926,14 @@
   The auxiliary data of this lemma can be retrieved using the function 
   @{ML_ind get_tags in Thm}. So far the the auxiliary data of this lemma is 
 
-  @{ML_response_fake [display,gray]
+  @{ML_matchresult_fake [display,gray]
   "Thm.get_tags @{thm foo_data}"
   "[(\"name\", \"General.foo_data\"), (\"kind\", \"lemma\")]"}
 
   consisting of a name and a kind.  When we store lemmas in the theorem database, 
   we might want to explicitly extend this data by attaching case names to the 
   two premises of the lemma.  This can be done with the function @{ML_ind name in Rule_Cases}
-  from the structure @{ML_struct Rule_Cases}.
+  from the structure @{ML_structure Rule_Cases}.
 \<close>
 
 local_setup %gray \<open>
@@ -1944,7 +1944,7 @@
 text \<open>
   The data of the theorem @{thm [source] foo_data'} is then as follows:
 
-  @{ML_response_fake [display,gray]
+  @{ML_matchresult_fake [display,gray]
   "Thm.get_tags @{thm foo_data'}"
   "[(\"name\", \"General.foo_data'\"), (\"kind\", \"lemma\"), 
  (\"case_names\", \"foo_case_one;foo_case_two\")]"}
@@ -1996,7 +1996,7 @@
   proving a theorem, especially when the proof is by \<open>auto\<close>. These theorems can be obtained by introspecting the proved theorem.
   To introspect a theorem, let us define the following three functions
   that analyse the @{ML_type_ind proof_body} data-structure from the
-  structure @{ML_struct Proofterm}.
+  structure @{ML_structure Proofterm}.
 \<close>
 
 ML %grayML\<open>fun pthms_of (PBody {thms, ...}) = map #2 thms 
@@ -2036,7 +2036,7 @@
   extracting this information.  Let us first extract the name of the
   established theorem. This can be done with
 
-  @{ML_response_fake [display,gray]
+  @{ML_matchresult_fake [display,gray]
   "@{thm my_conjIa}
   |> Thm.proof_body_of
   |> get_names"
@@ -2050,7 +2050,7 @@
   and @{thm [source] conjunct2}. We can obtain them by descending into the
   first level of the proof-tree, as follows.
 
-  @{ML_response_fake [display,gray]
+  @{ML_matchresult_fake [display,gray]
   "@{thm my_conjIa}
   |> Thm.proof_body_of
   |> get_pbodies
@@ -2064,7 +2064,7 @@
   proof in Isabelle. Note also that applications of \<open>assumption\<close> do not
   count as a separate theorem, as you can see in the following code.
 
-  @{ML_response_fake [display,gray]
+  @{ML_matchresult_fake [display,gray]
   "@{thm my_conjIb}
   |> Thm.proof_body_of
   |> get_pbodies
@@ -2077,7 +2077,7 @@
   and @{thm [source] my_conjIb}, as can be seen by the theorems that
   are returned for @{thm [source] my_conjIc}.
 
-  @{ML_response_fake [display,gray]
+  @{ML_matchresult_fake [display,gray]
   "@{thm my_conjIc}
   |> Thm.proof_body_of
   |> get_pbodies
@@ -2092,7 +2092,7 @@
   means we obtain the theorems that are used in order to prove
   @{thm [source] conjunct1}, @{thm [source] conjunct2} and @{thm [source] conjI}.
 
-  @{ML_response_fake [display, gray]
+  @{ML_matchresult_fake [display, gray]
   "@{thm my_conjIa}
   |> Thm.proof_body_of
   |> get_pbodies
@@ -2408,7 +2408,7 @@
 text \<open>
   then you can see it is added to the initially empty list.
 
-  @{ML_response_fake [display,gray]
+  @{ML_matchresult_fake [display,gray]
   "MyThms.get @{context}" 
   "[\"True\"]"}
 
@@ -2422,7 +2422,7 @@
   not need to be explicitly given. These three declarations will cause the 
   theorem list to be updated as:
 
-  @{ML_response_fake [display,gray]
+  @{ML_matchresult_fake [display,gray]
   "MyThms.get @{context}"
   "[\"True\", \"Suc (Suc 0) = 2\"]"}
 
@@ -2435,7 +2435,7 @@
 
 text \<open>After this, the theorem list is again: 
 
-  @{ML_response_fake [display,gray]
+  @{ML_matchresult_fake [display,gray]
   "MyThms.get @{context}"
   "[\"True\"]"}
 
@@ -2468,7 +2468,7 @@
   The function @{ML str in Pretty} transforms a (plain) string into such a pretty 
   type. For example
 
-  @{ML_response_fake [display,gray]
+  @{ML_matchresult_fake [display,gray]
   "Pretty.str \"test\"" "String (\"test\", 4)"}
 
   where the result indicates that we transformed a string with length 4. Once
@@ -2503,7 +2503,7 @@
   If we print out the string using the usual ``quick-and-dirty'' method, then
   we obtain the ugly output:
 
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "tracing test_str"
 "fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar foooooooooo
 ooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaa
@@ -2512,7 +2512,7 @@
 
   We obtain the same if we just use the function @{ML pprint}.
 
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "pprint (Pretty.str test_str)"
 "fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar foooooooooo
 ooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaa
@@ -2526,7 +2526,7 @@
   list. To print this list of pretty types as a single string, we concatenate
   them with the function @{ML_ind blk in Pretty} as follows:
 
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "let
   val ptrs = map Pretty.str (space_explode \" \" test_str)
 in
@@ -2542,7 +2542,7 @@
   indentation of the printed string. You can increase the indentation 
   and obtain
   
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "let
   val ptrs = map Pretty.str (space_explode \" \" test_str)
 in
@@ -2557,7 +2557,7 @@
   that every line starts with the same indent, you can use the
   function @{ML_ind  indent in Pretty} as follows:
 
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "let
   val ptrs = map Pretty.str (space_explode \" \" test_str)
 in
@@ -2572,7 +2572,7 @@
   have the linebreaks handled properly, you can use the function 
   @{ML_ind  commas in Pretty}. For example
 
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "let
   val ptrs = map (Pretty.str o string_of_int) (99998 upto 100020)
 in
@@ -2590,7 +2590,7 @@
 
 text \<open>
   
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "let
   val ptrs = map (Pretty.str o string_of_int) (99998 upto 100020)
 in
@@ -2629,7 +2629,7 @@
   can occur. We do the same after the @{text [quotes] "and"}. This gives you
   for example
 
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "let
   val ptrs1 = map (Pretty.str o string_of_int) (1 upto 22)
   val ptrs2 = map (Pretty.str o string_of_int) (10 upto 28)
@@ -2646,7 +2646,7 @@
   a list of items, but automatically inserts forced breaks between each item.
   Compare
 
-  @{ML_response_fake [display,gray]
+  @{ML_matchresult_fake [display,gray]
   "let
   val a_and_b = [Pretty.str \"a\", Pretty.str \"b\"]
 in
@@ -2661,7 +2661,7 @@
   It is used for example in the command \isacommand{print\_theorems}. An
   example is as follows.
 
-  @{ML_response_fake [display,gray]
+  @{ML_matchresult_fake [display,gray]
   "let
   val pstrs = map (Pretty.str o string_of_int) (4 upto 10)
 in
@@ -2681,7 +2681,7 @@
   out the the terms produced by the the function @{ML de_bruijn} from 
   exercise~\ref{ex:debruijn} we obtain the following: 
 
-  @{ML_response_fake [display,gray]
+  @{ML_matchresult_fake [display,gray]
   "pprint (Syntax.pretty_term  @{context} (de_bruijn 4))"
   "(P 3 = P 4 \<longrightarrow> P 4 \<and> P 3 \<and> P 2 \<and> P 1) \<and>
 (P 2 = P 3 \<longrightarrow> P 4 \<and> P 3 \<and> P 2 \<and> P 1) \<and>
@@ -2715,14 +2715,14 @@
   line break, because we do not want that a line break occurs there.
   Now you can write
 
-  @{ML_response_fake [display,gray]
+  @{ML_matchresult_fake [display,gray]
   "tell_type @{context} @{term \"min (Suc 0)\"}"
   "The term \"min (Suc 0)\" has type \"nat \<Rightarrow> nat\"."}
   
   To see the proper line breaking, you can try out the function on a bigger term 
   and type. For example:
 
-  @{ML_response_fake [display,gray]
+  @{ML_matchresult_fake [display,gray]
   "tell_type @{context} @{term \"(=) ((=) ((=) ((=) ((=) (=)))))\"}"
   "The term \"(=) ((=) ((=) ((=) ((=) (=)))))\" has type 
 \"((((('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool\"."}




