--- a/ProgTutorial/Recipes/Introspection.thy	Tue May 14 17:45:13 2019 +0200
+++ b/ProgTutorial/Recipes/Introspection.thy	Thu May 16 19:56:12 2019 +0200
@@ -13,7 +13,7 @@
 
   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}.
+  @{ML_structure Proofterm}.
 \<close>
 
 ML %grayML\<open>fun pthms_of (PBody {thms, ...}) = map #2 thms 
@@ -52,7 +52,7 @@
   extracting this information.  Let us first extract the name of the
   established theorem. This can be done with
 
-  @{ML_response [display,gray]
+  @{ML_matchresult [display,gray]
   "@{thm my_conjIa}
   |> Thm.proof_body_of
   |> get_names"
@@ -67,7 +67,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
@@ -82,7 +82,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
@@ -96,7 +96,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
@@ -112,7 +112,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
@@ -124,6 +124,9 @@
   "[\"\", \"Pure.protectD\",
  \"Pure.protectI\"]"}
 \<close>
+
+
+
 text \<open>
   \begin{readmore} 
   The data-structure @{ML_type proof_body} is implemented