--- a/ProgTutorial/Recipes/Introspection.thy	Fri Jun 03 15:15:17 2016 +0100
+++ b/ProgTutorial/Recipes/Introspection.thy	Tue May 14 11:10:53 2019 +0200
@@ -17,8 +17,8 @@
 *}
 
 ML %grayML{*fun pthms_of (PBody {thms, ...}) = map #2 thms 
-val get_names = map #1 o pthms_of 
-val get_pbodies = map (Future.join o #3) o pthms_of *}
+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 *}
 
 text {* 
   To see what their purpose is, consider the following three short proofs.
@@ -57,7 +57,8 @@
   |> Thm.proof_body_of
   |> get_names"
   "[\"Introspection.my_conjIa\"]"}
-
+*}
+text {*
   whereby @{text "Introspection"} refers to the theory name in which
   we established the theorem @{thm [source] my_conjIa}. The function @{ML_ind
   proof_body_of in Thm} returns a part of the data that is stored in a
@@ -66,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 [display,gray]
+  @{ML_response_fake [display,gray]
   "@{thm my_conjIa}
   |> Thm.proof_body_of
   |> get_pbodies
@@ -74,41 +75,44 @@
   |> List.concat"
   "[\"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.conjI\", \"Pure.protectD\", 
   \"Pure.protectI\"]"}
-
+*}
+text {*
   The theorems @{thm [source] protectD} and @{thm [source]
   protectI} that are internal theorems are always part of a
   proof in Isabelle. Note also that applications of @{text assumption} do not
   count as a separate theorem, as you can see in the following code.
 
-  @{ML_response [display,gray]
+  @{ML_response_fake [display,gray]
   "@{thm my_conjIb}
   |> Thm.proof_body_of
   |> get_pbodies
   |> map get_names
   |> List.concat"
   "[\"Pure.protectD\", \"Pure.protectI\"]"}
-
+*}
+text {*
   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_response [display,gray]
+  @{ML_response_fake [display,gray]
   "@{thm my_conjIc}
   |> Thm.proof_body_of
   |> get_pbodies
   |> map get_names
   |> List.concat"
-  "[\"HOL.Eq_TrueI\", \"HOL.simp_thms_25\", \"HOL.eq_reflection\",
-  \"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.TrueI\", \"Pure.protectD\",
-  \"Pure.protectI\"]"}
-
+  "[\"HOL.implies_True_equals\", \"HOL.Eq_TrueI\", \"HOL.simp_thms_25\", \"HOL.eq_reflection\", 
+    \"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.TrueI\", \"Pure.protectD\",
+    \"Pure.protectI\"]"}
+*}
+text {*
   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_response [display, gray]
+  @{ML_response_fake [display, gray]
   "@{thm my_conjIa}
   |> Thm.proof_body_of
   |> get_pbodies
@@ -116,10 +120,11 @@
   |> (map o map) get_names
   |> List.concat
   |> List.concat
-  |> duplicates (op=)"
-  "[\"HOL.spec\", \"HOL.and_def\", \"HOL.mp\", \"HOL.impI\", \"Pure.protectD\",
-  \"Pure.protectI\"]"}
-
+  |> duplicates (op =)"
+  "[\"\", \"Pure.protectD\",
+ \"Pure.protectI\"]"}
+*}
+text {*
   \begin{readmore} 
   The data-structure @{ML_type proof_body} is implemented
   in the file @{ML_file "Pure/proofterm.ML"}. The implementation