diff -r 95b42288294e -r 438703674711 ProgTutorial/Essential.thy
--- a/ProgTutorial/Essential.thy	Fri May 17 11:21:09 2019 +0200
+++ b/ProgTutorial/Essential.thy	Tue May 21 14:37:39 2019 +0200
@@ -45,6 +45,15 @@
 | Abs of string * typ * term 
 | $ of term * term\<close>
 
+ML \<open>
+let 
+  val redex = @{term "(\<lambda>(x::int) (y::int). x)"} 
+  val arg1 = @{term "1::int"} 
+  val arg2 = @{term "2::int"}
+in
+  pretty_term @{context} (redex $ arg1 $ arg2)
+end\<close>
+
 text \<open>
   This datatype implements Church-style lambda-terms, where types are
   explicitly recorded in variables, constants and abstractions.  The
@@ -53,7 +62,7 @@
   terms use the usual de Bruijn index mechanism for representing bound
   variables.  For example in
 
-  @{ML_matchresult_fake [display, gray]
+  @{ML_response [display, gray]
   \<open>@{term "\<lambda>x y. x y"}\<close>
   \<open>Abs ("x", "'a \<Rightarrow> 'b", Abs ("y", "'a", Bound 1 $ Bound 0))\<close>}
 
@@ -69,7 +78,7 @@
   Be careful if you pretty-print terms. Consider pretty-printing the abstraction
   term shown above:
 
-  @{ML_matchresult_fake [display, gray]
+  @{ML_response [display, gray]
 \<open>@{term "\<lambda>x y. x y"}
   |> pretty_term @{context}
   |> pwriteln\<close>
@@ -79,7 +88,7 @@
   tacitly eta-contracted the output. You obtain a similar result 
   with beta-redexes
 
-  @{ML_matchresult_fake [display, gray]
+  @{ML_response [display, gray]
 \<open>let 
   val redex = @{term "(\<lambda>(x::int) (y::int). x)"} 
   val arg1 = @{term "1::int"} 
@@ -97,7 +106,7 @@
   value @{ML_ind show_abbrevs in Syntax}. For example
 
 
-  @{ML_matchresult_fake [display, gray]
+  @{ML_response [display, gray]
   \<open>let 
   val redex = @{term "(\<lambda>(x::int) (y::int). x)"} 
   val arg1 = @{term "1::int"} 
@@ -114,7 +123,7 @@
   \emph{schematic} variables (term-constructor @{ML Var} and written with a
   leading question mark). Consider the following two examples
   
-  @{ML_matchresult_fake [display, gray]
+  @{ML_response [display, gray]
 \<open>let
   val v1 = Var (("x", 3), @{typ bool})
   val v2 = Var (("x1", 3), @{typ bool})
@@ -144,20 +153,20 @@
   Constructing terms via antiquotations has the advantage that only typable
   terms can be constructed. For example
 
-  @{ML_matchresult_fake_both [display,gray]
+  @{ML_response [display,gray]
   \<open>@{term "x x"}\<close>
   \<open>Type unification failed: Occurs check!\<close>}
 
   raises a typing error, while it is perfectly ok to construct the term
   with the raw ML-constructors:
 
-  @{ML_matchresult_fake [display,gray] 
+  @{ML_response [display,gray] 
 \<open>let
   val omega = Free ("x", @{typ "nat \<Rightarrow> nat"}) $ Free ("x", @{typ nat})
 in 
   pwriteln (pretty_term @{context} omega)
 end\<close>
-  \<open>x x\<close>}
+  "x x"}
   
   Sometimes the internal representation of terms can be surprisingly different
   from what you see at the user-level, because the layers of
@@ -204,7 +213,7 @@
   As already seen above, types can be constructed using the antiquotation 
   \<open>@{typ _}\<close>. For example:
 
-  @{ML_matchresult_fake [display,gray] \<open>@{typ "bool \<Rightarrow> nat"}\<close> \<open>bool \<Rightarrow> nat\<close>}
+  @{ML_response [display,gray] \<open>@{typ "bool \<Rightarrow> nat"}\<close> \<open>bool \<Rightarrow> nat\<close>}
 
   The corresponding datatype is
 \<close>
@@ -294,11 +303,11 @@
   After that the types for booleans, lists and so on are printed out again 
   the standard Isabelle way.
 
-  @{ML_matchresult_fake [display, gray]
-  \<open>@{typ "bool"};
-@{typ "'a list"}\<close>
-  \<open>"bool"
-"'a List.list"\<close>}
+  @{ML_response [display, gray]
+  \<open>(@{typ "bool"},
+@{typ "'a list"})\<close>
+  \<open>("bool",
+"'a list")\<close>}
 
   \begin{readmore}
   Types are described in detail in \isccite{sec:types}. Their
@@ -358,7 +367,7 @@
   term list applied to the term. For example
 
 
-@{ML_matchresult_fake [display,gray]
+@{ML_response [display,gray]
 \<open>let
   val trm = @{term "P::bool \<Rightarrow> bool \<Rightarrow> bool"}
   val args = [@{term "True"}, @{term "False"}]
@@ -366,19 +375,19 @@
   list_comb (trm, args)
 end\<close>
 \<open>Free ("P", "bool \<Rightarrow> bool \<Rightarrow> bool") 
-   $ Const ("True", "bool") $ Const ("False", "bool")\<close>}
+   $ Const ("HOL.True", "bool") $ Const ("HOL.False", "bool")\<close>}
 
   Another handy function is @{ML_ind lambda in Term}, which abstracts a variable 
   in a term. For example
 
-  @{ML_matchresult_fake [display,gray]
+  @{ML_response [display,gray]
 \<open>let
   val x_nat = @{term "x::nat"}
   val trm = @{term "(P::nat \<Rightarrow> bool) x"}
 in
   lambda x_nat trm
 end\<close>
-  \<open>Abs ("x", "Nat.nat", Free ("P", "bool \<Rightarrow> bool") $ Bound 0)\<close>}
+  \<open>Abs ("x", "nat", Free ("P", "nat \<Rightarrow> bool") $ Bound 0)\<close>}
 
   In this example, @{ML lambda} produces a de Bruijn index (i.e.\ @{ML \<open>Bound 0\<close>}), 
   and an abstraction, where it also records the type of the abstracted
@@ -387,7 +396,7 @@
   is of the same type as the abstracted variable. If it is of different type,
   as in
 
-  @{ML_matchresult_fake [display,gray]
+  @{ML_response [display,gray]
 \<open>let
   val x_int = @{term "x::int"}
   val trm = @{term "(P::nat \<Rightarrow> bool) x"}
@@ -406,7 +415,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_matchresult_fake [display,gray]
+  @{ML_response [display,gray]
 \<open>let
   val sub1 = (@{term "(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0"}, @{term "y::nat \<Rightarrow> nat"})
   val sub2 = (@{term "x::nat"}, @{term "True"})
@@ -414,12 +423,12 @@
 in
   subst_free [sub1, sub2] trm
 end\<close>
-  \<open>Free ("y", "nat \<Rightarrow> nat") $ Const ("True", "bool")\<close>}
+  \<open>Free ("y", "nat \<Rightarrow> nat") $ Const ("HOL.True", "bool")\<close>}
 
   As can be seen, @{ML subst_free} does not take typability into account.
   However it takes alpha-equivalence into account:
 
-  @{ML_matchresult_fake [display, gray]
+  @{ML_response [display, gray]
 \<open>let
   val sub = (@{term "(\<lambda>y::nat. y)"}, @{term "x::nat"})
   val trm = @{term "(\<lambda>x::nat. x)"}
@@ -446,10 +455,10 @@
   The function returns a pair consisting of the stripped off variables and
   the body of the universal quantification. For example
 
-  @{ML_matchresult_fake [display, gray]
+  @{ML_response [display, gray]
   \<open>strip_alls @{term "\<forall>x y. x = (y::bool)"}\<close>
 \<open>([Free ("x", "bool"), Free ("y", "bool")],
-  Const ("op =", _) $ Bound 1 $ Bound 0)\<close>}
+  Const ("HOL.eq",\<dots>) $ Bound 1 $ Bound 0)\<close>}
 
   Note that we produced in the body two dangling de Bruijn indices. 
   Later on we will also use the inverse function that
@@ -466,7 +475,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_matchresult_fake [display, gray, linenos]
+  @{ML_response [display, gray, linenos]
   \<open>let
   val (vrs, trm) = strip_alls @{term "\<forall>x y. x = (y::bool)"}
 in 
@@ -488,20 +497,20 @@
   the loose de Bruijn index is replaced by a unique free variable. For example
 
 
-  @{ML_matchresult_fake [display,gray]
+  @{ML_response [display,gray]
   \<open>let
   val body = Bound 0 $ Free ("x", @{typ nat})
 in
   Term.dest_abs ("x", @{typ "nat \<Rightarrow> bool"}, body)
 end\<close>
-  \<open>("xa", Free ("xa", "Nat.nat \<Rightarrow> bool") $ Free ("x", "Nat.nat"))\<close>}
+  \<open>("xa", Free ("xa", "nat \<Rightarrow> bool") $ Free ("x", "nat"))\<close>}
 
   Sometimes it is necessary to manipulate de Bruijn indices in terms directly.
   There are many functions to do this. We describe only two. The first,
   @{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_matchresult_fake [display,gray]
+@{ML_response [display,gray]
 \<open>@{term "\<forall>x y z u. z = u"}
   |> strip_alls
   ||> incr_boundvars 2
@@ -519,7 +528,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_matchresult_fake [gray,display]
+  @{ML_matchresult [gray,display]
 \<open>let
   val body = snd (strip_alls @{term "\<forall>x y. x = (y::bool)"})
 in
@@ -534,7 +543,7 @@
   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_matchresult_fake [gray,display]
+@{ML_response [gray,display]
 \<open>let
   val eq = HOLogic.mk_eq (@{term "True"}, @{term "False"})
 in
@@ -674,10 +683,10 @@
 text \<open>
   Here is an example:
 
-@{ML_matchresult_fake [display,gray] 
+@{ML_response [display,gray] 
 \<open>map_types nat_to_int @{term "a = (1::nat)"}\<close> 
-\<open>Const ("op =", "int \<Rightarrow> int \<Rightarrow> bool")
-           $ Free ("a", "int") $ Const ("HOL.one_class.one", "int")\<close>}
+\<open>Const ("HOL.eq", "int \<Rightarrow> int \<Rightarrow> bool")
+           $ Free ("a", "int") $ Const ("Groups.one_class.one", "int")\<close>}
 
   If you want to obtain the list of free type-variables of a term, you
   can use the function @{ML_ind  add_tfrees in Term} 
@@ -798,9 +807,9 @@
   @{ML tyenv_unif} with the built-in function @{ML_ind dest in Vartab} from the
   structure @{ML_structure Vartab}.
 
-  @{ML_matchresult_fake [display,gray]
+  @{ML_response [display,gray]
   \<open>Vartab.dest tyenv_unif\<close>
-  \<open>[(("'a", 0), (["HOL.type"], "?'b List.list")), 
+  \<open>[(("'a", 0), (["HOL.type"], "?'b list")), 
  (("'b", 0), (["HOL.type"], "nat"))]\<close>} 
 \<close>
 
@@ -839,7 +848,7 @@
   environment in the example this function prints out the more legible:
 
 
-  @{ML_matchresult_fake [display, gray]
+  @{ML_response [display, gray]
   \<open>pretty_tyenv @{context} tyenv_unif\<close>
   \<open>[?'a := ?'b list, ?'b := nat]\<close>}
 
@@ -877,15 +886,21 @@
   Sign.typ_unify @{theory} (ty1, ty2) (Vartab.empty, 0) 
 end\<close>
 
+declare[[show_sorts]]
+
 text \<open>
   To print out the result type environment we switch on the printing 
   of sort information by setting @{ML_ind show_sorts in Syntax} to 
   true. This allows us to inspect the typing environment.
 
-  @{ML_matchresult_fake [display,gray]
+  @{ML_response [display,gray]
   \<open>pretty_tyenv @{context} tyenv\<close>
   \<open>[?'a::s1 := ?'a1::{s1, s2}, ?'b::s2 := ?'a1::{s1, s2}]\<close>}
-
+\<close>
+
+declare[[show_sorts=false]]
+
+text\<open>
   As can be seen, the type variables \<open>?'a\<close> and \<open>?'b\<close> are instantiated
   with a new type variable \<open>?'a1\<close> with sort \<open>{s1, s2}\<close>. Since a new
   type variable has been introduced the @{ML index}, originally being \<open>0\<close>, 
@@ -899,7 +914,7 @@
   \<open>?'b list * nat\<close> from the beginning of this section, and the 
   calculated type environment @{ML tyenv_unif}:
 
-  @{ML_matchresult_fake [display, gray]
+  @{ML_response [display, gray]
   \<open>pretty_tyenv @{context} tyenv_unif\<close>
   \<open>[?'a := ?'b list, ?'b := nat]\<close>}
 
@@ -911,9 +926,9 @@
   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_matchresult_fake [display, gray]
+  @{ML_response [display, gray]
   \<open>Envir.norm_type tyenv_unif @{typ_pat "?'a * ?'b"}\<close>
-  \<open>nat list * nat\<close>}
+  \<open>nat list \<times> nat\<close>}
 
   Matching of types can be done with the function @{ML_ind typ_match in Sign}
   also from the structure @{ML_structure Sign}. This function returns a @{ML_type
@@ -931,7 +946,7 @@
 text \<open>
   Printing out the calculated matcher gives
 
-  @{ML_matchresult_fake [display,gray]
+  @{ML_response [display,gray]
   \<open>pretty_tyenv @{context} tyenv_match\<close>
   \<open>[?'a := bool list, ?'b := nat]\<close>}
   
@@ -939,9 +954,9 @@
   applying the matcher to a type needs to be done with the function
   @{ML_ind subst_type in Envir}. For example
 
-  @{ML_matchresult_fake [display, gray]
+  @{ML_response [display, gray]
   \<open>Envir.subst_type tyenv_match @{typ_pat "?'a * ?'b"}\<close>
-  \<open>bool list * nat\<close>}
+  \<open>bool list \<times> nat\<close>}
 
   Be careful to observe the difference: always use
   @{ML subst_type in Envir} for matchers and @{ML norm_type in Envir} 
@@ -960,16 +975,16 @@
   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_matchresult_fake [display, gray]
+  @{ML_response [display, gray]
   \<open>Envir.norm_type tyenv_match' @{typ_pat "?'a * ?'b"}\<close>
-  \<open>nat list * nat\<close>}
+  \<open>nat list \<times> nat\<close>}
 
   which does not solve the matching problem, and if
   we apply @{ML subst_type in Envir} to the same type we obtain
 
-  @{ML_matchresult_fake [display, gray]
+  @{ML_response [display, gray]
   \<open>Envir.subst_type tyenv_unif @{typ_pat "?'a * ?'b"}\<close>
-  \<open>?'b list * nat\<close>}
+  \<open>?'b list \<times> nat\<close>}
   
   which does not solve the unification problem.
 
@@ -1023,7 +1038,7 @@
   the type environment is empty and can be ignored. The 
   resulting term environment is
 
-  @{ML_matchresult_fake [display, gray]
+  @{ML_response [display, gray]
   \<open>pretty_env @{context} fo_env\<close>
   \<open>[?X := P, ?Y := \<lambda>a b. Q b a]\<close>}
 
@@ -1033,7 +1048,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_matchresult_fake [display, gray]
+  @{ML_response [display, gray]
   \<open>let
   val trm = @{term_pat "(?X::(nat\<Rightarrow>nat\<Rightarrow>nat)\<Rightarrow>bool) ?Y"}
 in
@@ -1050,7 +1065,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_matchresult_fake [display, gray]
+  @{ML_response [display, gray]
   \<open>let
   val fo_pat = @{term_pat "\<lambda>y. (?X::nat\<Rightarrow>bool) y"}
   val trm = @{term "\<lambda>x. (P::nat\<Rightarrow>bool) x"} 
@@ -1101,7 +1116,7 @@
   and @{ML_ind unify in Pattern}, both implemented in the structure
   @{ML_structure Pattern}. An example for higher-order pattern unification is
 
-  @{ML_matchresult_fake [display, gray]
+  @{ML_response [display, gray]
   \<open>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,13 +1167,15 @@
 
   We can print them out as follows.
 
-  @{ML_matchresult_fake [display, gray]
-  \<open>pretty_env @{context} (Envir.term_env un1);
-pretty_env @{context} (Envir.term_env un2);
-pretty_env @{context} (Envir.term_env un3)\<close>
-  \<open>[?X := \<lambda>a. a, ?Y := f a]
-[?X := f, ?Y := a]
-[?X := \<lambda>b. f a]\<close>}
+  @{ML_response [display, gray]
+  \<open>pretty_env @{context} (Envir.term_env un1)\<close>
+  \<open>[?X := \<lambda>a. a, ?Y := f a]\<close>}
+  @{ML_response [display, gray]
+  \<open>pretty_env @{context} (Envir.term_env un2)\<close>
+  \<open>[?X := f, ?Y := a]\<close>}
+  @{ML_response [display, gray]
+  \<open>pretty_env @{context} (Envir.term_env un3)\<close>
+  \<open>[?X := \<lambda>b. f a]\<close>}
 
 
   In case of failure the function @{ML_ind unifiers in Unify} does not raise
@@ -1181,9 +1198,9 @@
   called. This function has a built-in bound, which can be accessed and
   manipulated as a configuration value. For example
 
-  @{ML_matchresult_fake [display,gray]
+  @{ML_matchresult [display,gray]
   \<open>Config.get_global @{theory} (Unify.search_bound)\<close>
-  \<open>Int 60\<close>}
+  \<open>60\<close>}
 
   If this bound is reached during unification, Isabelle prints out the
   warning message @{text [quotes] "Unification bound exceeded"} and
@@ -1266,7 +1283,7 @@
   @{term "Q True"}. 
  
 
-  @{ML_matchresult_fake [gray,display,linenos] 
+  @{ML_response [gray,display,linenos] 
   \<open>let  
   val pat = Logic.strip_imp_concl (Thm.prop_of @{thm spec})
   val trm = @{term "Trueprop (Q True)"}
@@ -1361,9 +1378,9 @@
   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_matchresult_fake [display,gray] 
+  @{ML_response [display,gray] 
   \<open>type_of (@{term "f::nat \<Rightarrow> bool"} $ @{term "x::int"})\<close> 
-  \<open>*** Exception- TYPE ("type_of: type mismatch in application" \<dots>\<close>}
+  \<open>exception TYPE raised \<dots>\<close>}
 
   Since the complete traversal might sometimes be too costly and
   not necessary, there is the function @{ML_ind fastype_of in Term}, which 
@@ -1387,7 +1404,7 @@
   complete type. The type inference can be invoked with the function
   @{ML_ind check_term in Syntax}. An example is as follows:
 
-  @{ML_matchresult_fake [display,gray] 
+  @{ML_response [display,gray] 
 \<open>let
   val c = Const (@{const_name "plus"}, dummyT) 
   val o = @{term "1::nat"} 
@@ -1395,8 +1412,8 @@
 in   
   Syntax.check_term @{context} (c $ o $ v)
 end\<close>
-\<open>Const ("HOL.plus_class.plus", "nat \<Rightarrow> nat \<Rightarrow> nat") $
-  Const ("HOL.one_class.one", "nat") $ Free ("x", "nat")\<close>}
+\<open>Const ("Groups.plus_class.plus", "nat \<Rightarrow> nat \<Rightarrow> nat") $
+  Const ("Groups.one_class.one", "nat") $ Free ("x", "nat")\<close>}
 
   Instead of giving explicitly the type for the constant \<open>plus\<close> and the free 
   variable \<open>x\<close>, type-inference fills in the missing information.
@@ -1432,26 +1449,26 @@
   Certification is always relative to a context. For example you can 
   write:
 
-  @{ML_matchresult_fake [display,gray] 
+  @{ML_response [display,gray] 
   \<open>Thm.cterm_of @{context} @{term "(a::nat) + b = c"}\<close> 
   \<open>a + b = c\<close>}
 
   This can also be written with an antiquotation:
 
-  @{ML_matchresult_fake [display,gray] 
+  @{ML_response [display,gray] 
   \<open>@{cterm "(a::nat) + b = c"}\<close> 
   \<open>a + b = c\<close>}
 
   Attempting to obtain the certified term for
 
-  @{ML_matchresult_fake_both [display,gray] 
+  @{ML_response [display,gray] 
   \<open>@{cterm "1 + True"}\<close> 
-  \<open>Type unification failed \<dots>\<close>}
+  \<open>Type unification failed\<dots>\<close>}
 
   yields an error (since the term is not typable). A slightly more elaborate
   example that type-checks is:
 
-@{ML_matchresult_fake [display,gray] 
+@{ML_response [display,gray] 
 \<open>let
   val natT = @{typ "nat"}
   val zero = @{term "0::nat"}
@@ -1465,13 +1482,13 @@
   you obtain the certified type for the Isabelle type @{typ "nat \<Rightarrow> bool"} on 
   the ML-level as follows:
 
-  @{ML_matchresult_fake [display,gray]
+  @{ML_response [display,gray]
   \<open>Thm.ctyp_of @{context} (@{typ nat} --> @{typ bool})\<close>
   \<open>nat \<Rightarrow> bool\<close>}
 
   or with the antiquotation:
 
-  @{ML_matchresult_fake [display,gray]
+  @{ML_response [display,gray]
   \<open>@{ctyp "nat \<Rightarrow> bool"}\<close>
   \<open>nat \<Rightarrow> bool\<close>}
 
@@ -1479,14 +1496,14 @@
   pattern-match against them. However, we can construct them. For example
   the function @{ML_ind apply in Thm} produces a certified application.
 
-  @{ML_matchresult_fake [display,gray]
+  @{ML_response [display,gray]
   \<open>Thm.apply @{cterm "P::nat \<Rightarrow> bool"} @{cterm "3::nat"}\<close>
   \<open>P 3\<close>}
 
   Similarly the function @{ML_ind list_comb in Drule} from the structure @{ML_structure Drule}
   applies a list of @{ML_type cterm}s.
 
-  @{ML_matchresult_fake [display,gray]
+  @{ML_response [display,gray]
   \<open>let
   val chead = @{cterm "P::unit \<Rightarrow> nat \<Rightarrow> bool"}
   val cargs = [@{cterm "()"}, @{cterm "3::nat"}]
@@ -1546,7 +1563,7 @@
   If we print out the value of @{ML my_thm} then we see only the 
   final statement of the theorem.
 
-  @{ML_matchresult_fake [display, gray]
+  @{ML_response [display, gray]
   \<open>pwriteln (pretty_thm @{context} my_thm)\<close>
   \<open>\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t\<close>}
 
@@ -1725,14 +1742,14 @@
   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_matchresult_fake [display,gray]
+  @{ML_response [display,gray]
   \<open>let
   val eq = @{thm True_def}
 in
   (Thm.lhs_of eq, Thm.rhs_of eq) 
-  |> apply2 (Pretty.string_of o (pretty_cterm @{context}))
+  |> apply2 (YXML.content_of o Pretty.string_of o (pretty_cterm @{context}))
 end\<close>
-  \<open>(True, (\<lambda>x. x) = (\<lambda>x. x))\<close>}
+  \<open>("True", "(\<lambda>x. x) = (\<lambda>x. x)")\<close>}
 
   Other function produce terms that can be pattern-matched. 
   Suppose the following two theorems.
@@ -1778,7 +1795,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_matchresult_fake [display,gray,linenos]
+  @{ML_response [display,gray,linenos]
   \<open>Thm.reflexive @{cterm "True"}
   |> Simplifier.rewrite_rule @{context} [@{thm True_def}]
   |> pretty_thm @{context}
@@ -1795,14 +1812,14 @@
   @{ML_ind rulify in Object_Logic} 
   replaces all object connectives by equivalents in the meta logic. For example
 
-  @{ML_matchresult_fake [display, gray]
+  @{ML_response [display, gray]
   \<open>Object_Logic.rulify @{context} @{thm foo_test2}\<close>
   \<open>\<lbrakk>?A; ?B\<rbrakk> \<Longrightarrow> ?C\<close>}
 
   The transformation in the other direction can be achieved with function
   @{ML_ind atomize in Object_Logic} and the following code.
 
-  @{ML_matchresult_fake [display,gray]
+  @{ML_response [display,gray]
   \<open>let
   val thm = @{thm foo_test1}
   val meta_eq = Object_Logic.atomize @{context} (Thm.cprop_of thm)
@@ -1837,16 +1854,16 @@
 text \<open>
   This function produces for the theorem @{thm [source] list.induct}
 
-  @{ML_matchresult_fake [display, gray]
+  @{ML_response [display, gray]
   \<open>atomize_thm @{context} @{thm list.induct}\<close>
-  \<open>\<forall>P list. P [] \<longrightarrow> (\<forall>a list. P list \<longrightarrow> P (a # list)) \<longrightarrow> P list\<close>}
+  \<open>"\<forall>P list. P [] \<longrightarrow> (\<forall>x1 x2. P x2 \<longrightarrow> P (x1 # x2)) \<longrightarrow> P list"\<close>}
 
   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_structure Goal}. For example below we use this function
   to prove the term @{term "P \<Longrightarrow> P"}.
   
-  @{ML_matchresult_fake [display,gray]
+  @{ML_response [display,gray]
   \<open>let
   val trm = @{term "P \<Longrightarrow> P::bool"}
   val tac = K (assume_tac @{context} 1)
@@ -1868,17 +1885,17 @@
 \<close>
 
 ML %grayML\<open>fun rep_goals i = replicate i @{prop "f x = f x"}
-fun rep_tacs i = replicate i (resolve_tac @{context} [@{thm refl}])
+fun rep_tacs ctxt i = replicate i (resolve_tac ctxt [@{thm refl}])
 
 fun multi_test ctxt i =
   Goal.prove_common ctxt NONE ["f", "x"] [] (rep_goals i) 
-    (K ((Goal.conjunction_tac THEN' RANGE (rep_tacs i)) 1))\<close>
+    (K ((Goal.conjunction_tac THEN' RANGE (rep_tacs ctxt i)) 1))\<close>
 
 text \<open>
   With them we can now produce three theorem instances of the 
   proposition.
 
-  @{ML_matchresult_fake [display, gray]
+  @{ML_response [display, gray]
   \<open>multi_test @{context} 3\<close>
   \<open>["?f ?x = ?f ?x", "?f ?x = ?f ?x", "?f ?x = ?f ?x"]\<close>}
 
@@ -1903,7 +1920,7 @@
   purposes, or when explicit proof construction should be omitted due to performace 
   reasons. An example of this function is as follows:
 
-  @{ML_matchresult_fake [display, gray]
+  @{ML_response [display, gray]
   \<open>Skip_Proof.make_thm @{theory} @{prop "True = False"}\<close>
   \<open>True = False\<close>}
 
@@ -1919,16 +1936,16 @@
   Thm}. Assume you prove the following lemma.
 \<close>
 
-lemma foo_data: 
+theorem foo_data: 
   shows "P \<Longrightarrow> P \<Longrightarrow> P" by assumption
 
 text \<open>
   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_matchresult_fake [display,gray]
+  @{ML_matchresult [display,gray]
   \<open>Thm.get_tags @{thm foo_data}\<close>
-  \<open>[("name", "General.foo_data"), ("kind", "lemma")]\<close>}
+  \<open>[("name", "Essential.foo_data"), ("kind", "theorem")]\<close>}
 
   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 
@@ -1944,10 +1961,10 @@
 text \<open>
   The data of the theorem @{thm [source] foo_data'} is then as follows:
 
-  @{ML_matchresult_fake [display,gray]
+  @{ML_matchresult [display,gray]
   \<open>Thm.get_tags @{thm foo_data'}\<close>
-  \<open>[("name", "General.foo_data'"), ("kind", "lemma"), 
- ("case_names", "foo_case_one;foo_case_two")]\<close>}
+  \<open>[("name", "Essential.foo_data'"), 
+ ("case_names", "foo_case_one;foo_case_two"), ("kind", "theorem")]\<close>}
 
   You can observe the case names of this lemma on the user level when using 
   the proof methods \<open>cases\<close> and \<open>induct\<close>. In the proof below
@@ -2001,12 +2018,22 @@
 
 ML %grayML\<open>fun pthms_of (PBody {thms, ...}) = map #2 thms 
 val get_names = (map Proofterm.thm_node_name) o pthms_of 
-val get_pbodies = map (Future.join o Proofterm.thm_node_body) o pthms_of\<close>
+val get_pbodies = map (Future.join o Proofterm.thm_node_body) o pthms_of
+fun get_all_names thm =
+let
+  (*proof body with digest*)
+  val body = Proofterm.strip_thm (Thm.proof_body_of thm);
+  (*all theorems used in the graph of nested proofs*)
+in Proofterm.fold_body_thms
+     (fn {name, ...} => insert (op =) name) [body] []
+end\<close>
 
 text \<open>
   To see what their purpose is, consider the following three short proofs.
 \<close>
-
+ML \<open>
+
+\<close>
 lemma my_conjIa:
 shows "A \<and> B \<Longrightarrow> A \<and> B"
 apply(rule conjI)
@@ -2026,7 +2053,9 @@
 apply(auto)
 done
 
-
+ML "Proofterm.proofs"
+ML \<open>@{thm my_conjIa}
+  |> get_all_names\<close>
 text \<open>
   While the information about which theorems are used is obvious in
   the first two proofs, it is not obvious in the third, because of the
@@ -2036,7 +2065,7 @@
   extracting this information.  Let us first extract the name of the
   established theorem. This can be done with
 
-  @{ML_matchresult_fake [display,gray]
+  @{ML_matchresult [display,gray]
   \<open>@{thm my_conjIa}
   |> Thm.proof_body_of
   |> get_names\<close>
@@ -2048,61 +2077,44 @@
   theorem.  Notice that the first proof above references
   three theorems, namely @{thm [source] conjI}, @{thm [source] conjunct1} 
   and @{thm [source] conjunct2}. We can obtain them by descending into the
-  first level of the proof-tree, as follows.
-
-  @{ML_matchresult_fake [display,gray]
+  proof-tree. The function @{ML get_all_names} recursively selects all names.
+
+  @{ML_response [display,gray]
   \<open>@{thm my_conjIa}
-  |> Thm.proof_body_of
-  |> get_pbodies
-  |> map get_names
-  |> List.concat\<close>
-  \<open>["HOL.conjunct2", "HOL.conjunct1", "HOL.conjI", "Pure.protectD", 
-  "Pure.protectI"]\<close>}
+  |> get_all_names |> sort string_ord\<close>
+  \<open>["", "HOL.All_def", "HOL.FalseE", "HOL.False_def", "HOL.TrueI", "HOL.True_def", 
+   "HOL.True_or_False", "HOL.allI", "HOL.and_def", "HOL.conjI",
+   "HOL.conjunct1", "HOL.conjunct2", "HOL.disjE", "HOL.eqTrueE", "HOL.eqTrueI", 
+   "HOL.ext", "HOL.fun_cong", "HOL.iffD1", "HOL.iffD2", "HOL.iffI",
+   "HOL.impI", "HOL.mp", "HOL.or_def", "HOL.refl", "HOL.rev_iffD1", 
+   "HOL.rev_iffD2", "HOL.spec", "HOL.ssubst", "HOL.subst", "HOL.sym",
+   "Pure.protectD", "Pure.protectI"]\<close>}
 
   The theorems @{thm [source] Pure.protectD} and @{thm [source]
   Pure.protectI} that are internal theorems are always part of a
-  proof in Isabelle. Note also that applications of \<open>assumption\<close> do not
+  proof in Isabelle. The other theorems are the theorems used in the proofs of the theorems
+  @{thm [source] conjunct1}, @{thm [source] conjunct2} and @{thm [source] conjI}. 
+
+  Note also that applications of \<open>assumption\<close> do not
   count as a separate theorem, as you can see in the following code.
 
-  @{ML_matchresult_fake [display,gray]
+  @{ML_matchresult [display,gray]
   \<open>@{thm my_conjIb}
-  |> Thm.proof_body_of
-  |> get_pbodies
-  |> map get_names
-  |> List.concat\<close>
-  \<open>["Pure.protectD", "Pure.protectI"]\<close>}
+  |> get_all_names |> sort string_ord\<close>
+  \<open>["", "Pure.protectD", "Pure.protectI"]\<close>}
+
 
   Interestingly, but not surprisingly, the proof of @{thm [source]
   my_conjIc} procceeds quite differently from @{thm [source] my_conjIa}
   and @{thm [source] my_conjIb}, as can be seen by the theorems that
   are returned for @{thm [source] my_conjIc}.
-
-  @{ML_matchresult_fake [display,gray]
+ 
+  @{ML_response [display,gray]
   \<open>@{thm my_conjIc}
-  |> Thm.proof_body_of
-  |> get_pbodies
-  |> map get_names
-  |> List.concat\<close>
-  \<open>["HOL.Eq_TrueI", "HOL.simp_thms_25", "HOL.eq_reflection",
-  "HOL.conjunct2", "HOL.conjunct1", "HOL.TrueI", "Pure.protectD",
-  "Pure.protectI"]\<close>}
-
-  Of course we can also descend into the second level of the tree 
-  ``behind'' @{thm [source] my_conjIa} say, which
-  means we obtain the theorems that are used in order to prove
-  @{thm [source] conjunct1}, @{thm [source] conjunct2} and @{thm [source] conjI}.
-
-  @{ML_matchresult_fake [display, gray]
-  \<open>@{thm my_conjIa}
-  |> Thm.proof_body_of
-  |> get_pbodies
-  |> map get_pbodies
-  |> (map o map) get_names
-  |> List.concat
-  |> List.concat
-  |> duplicates (op=)\<close>
-  \<open>["HOL.spec", "HOL.and_def", "HOL.mp", "HOL.impI", "Pure.protectD",
-  "Pure.protectI"]\<close>}
+  |> get_all_names\<close>
+  \<open>["HOL.simp_thms_25", "Pure.conjunctionD1", "Pure.conjunctionD2", "Pure.conjunctionI", 
+    "HOL.rev_mp", "HOL.exI", "HOL.allE", "HOL.exE",\<dots>]\<close>}
+
 
   \begin{exercise}
   Have a look at the theorems that are used when a lemma is ``proved''
@@ -2408,7 +2420,7 @@
 text \<open>
   then you can see it is added to the initially empty list.
 
-  @{ML_matchresult_fake [display,gray]
+  @{ML_response [display,gray]
   \<open>MyThms.get @{context}\<close> 
   \<open>["True"]\<close>}
 
@@ -2422,7 +2434,7 @@
   not need to be explicitly given. These three declarations will cause the 
   theorem list to be updated as:
 
-  @{ML_matchresult_fake [display,gray]
+  @{ML_response [display,gray]
   \<open>MyThms.get @{context}\<close>
   \<open>["True", "Suc (Suc 0) = 2"]\<close>}
 
@@ -2435,7 +2447,7 @@
 
 text \<open>After this, the theorem list is again: 
 
-  @{ML_matchresult_fake [display,gray]
+  @{ML_response [display,gray]
   \<open>MyThms.get @{context}\<close>
   \<open>["True"]\<close>}
 
@@ -2482,7 +2494,7 @@
 \<close>
 
 ML %grayML\<open>fun pprint prt = tracing (Pretty.string_of prt)\<close>
-
+ML %invisible\<open>val pprint = YXML.content_of o Pretty.string_of\<close>
 text \<open>
   The point of the pretty-printing infrastructure is to give hints about how to
   layout text and let Isabelle do the actual layout. Let us first explain
@@ -2512,7 +2524,7 @@
 
   We obtain the same if we just use the function @{ML pprint}.
 
-@{ML_matchresult_fake [display,gray]
+@{ML_response [display,gray]
 \<open>pprint (Pretty.str test_str)\<close>
 \<open>fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar foooooooooo
 ooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaa
@@ -2526,7 +2538,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_matchresult_fake [display,gray]
+@{ML_response [display,gray]
 \<open>let
   val ptrs = map Pretty.str (space_explode " " test_str)
 in
@@ -2542,7 +2554,7 @@
   indentation of the printed string. You can increase the indentation 
   and obtain
   
-@{ML_matchresult_fake [display,gray]
+@{ML_response [display,gray]
 \<open>let
   val ptrs = map Pretty.str (space_explode " " test_str)
 in
@@ -2557,7 +2569,7 @@
   that every line starts with the same indent, you can use the
   function @{ML_ind  indent in Pretty} as follows:
 
-@{ML_matchresult_fake [display,gray]
+@{ML_response [display,gray]
 \<open>let
   val ptrs = map Pretty.str (space_explode " " test_str)
 in
@@ -2572,7 +2584,7 @@
   have the linebreaks handled properly, you can use the function 
   @{ML_ind  commas in Pretty}. For example
 
-@{ML_matchresult_fake [display,gray]
+@{ML_response [display,gray]
 \<open>let
   val ptrs = map (Pretty.str o string_of_int) (99998 upto 100020)
 in
@@ -2590,7 +2602,7 @@
 
 text \<open>
   
-@{ML_matchresult_fake [display,gray]
+@{ML_response [display,gray]
 \<open>let
   val ptrs = map (Pretty.str o string_of_int) (99998 upto 100020)
 in
@@ -2629,39 +2641,48 @@
   can occur. We do the same after the @{text [quotes] "and"}. This gives you
   for example
 
-@{ML_matchresult_fake [display,gray]
+@{ML_response [display,gray]
 \<open>let
   val ptrs1 = map (Pretty.str o string_of_int) (1 upto 22)
+in
+  pprint (Pretty.blk (0, and_list ptrs1))
+end\<close>
+\<open>1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21 
+and 22\<close>}
+@{ML_response [display,gray]
+\<open>let
   val ptrs2 = map (Pretty.str o string_of_int) (10 upto 28)
 in
-  pprint (Pretty.blk (0, and_list ptrs1));
   pprint (Pretty.blk (0, and_list ptrs2))
 end\<close>
-\<open>1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21 
-and 22
-10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27 and
+\<open>10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27 and
 28\<close>}
 
   Like @{ML blk in Pretty}, the function @{ML_ind chunks in Pretty} prints out 
   a list of items, but automatically inserts forced breaks between each item.
   Compare
 
-  @{ML_matchresult_fake [display,gray]
+  @{ML_response [display,gray]
   \<open>let
   val a_and_b = [Pretty.str "a", Pretty.str "b"]
 in
-  pprint (Pretty.blk (0, a_and_b));
+  pprint (Pretty.blk (0, a_and_b))
+end\<close>
+\<open>ab\<close>}
+ @{ML_response [display,gray]
+  \<open>let
+  val a_and_b = [Pretty.str "a", Pretty.str "b"]
+in
   pprint (Pretty.chunks a_and_b)
 end\<close>
-\<open>ab
-a
+\<open>a
 b\<close>}
 
   The function @{ML_ind big_list in Pretty} helps with printing long lists.
   It is used for example in the command \isacommand{print\_theorems}. An
   example is as follows.
 
-  @{ML_matchresult_fake [display,gray]
+  @{ML_response [display,gray]
   \<open>let
   val pstrs = map (Pretty.str o string_of_int) (4 upto 10)
 in
@@ -2681,7 +2702,7 @@
   out the the terms produced by the the function @{ML de_bruijn} from 
   exercise~\ref{ex:debruijn} we obtain the following: 
 
-  @{ML_matchresult_fake [display,gray]
+  @{ML_response [display,gray]
   \<open>pprint (Syntax.pretty_term  @{context} (de_bruijn 4))\<close>
   \<open>(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>