--- a/ProgTutorial/Essential.thy	Fri Jun 22 19:55:20 2012 +0100
+++ b/ProgTutorial/Essential.thy	Mon Aug 27 10:24:10 2012 +0100
@@ -1322,6 +1322,8 @@
 
 ML {* Sign.classes_of @{theory} *}
 
+ML {* Sign.of_sort @{theory} *}
+
 text {*
   \begin{readmore}
   Classes, sorts and arities are defined in @{ML_file "Pure/term.ML"}.
@@ -2014,6 +2016,7 @@
 apply(auto)
 done
 
+
 text {*
   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
@@ -2023,7 +2026,7 @@
   extracting this information.  Let us first extract the name of the
   established theorem. This can be done with
 
-  @{ML_response [display,gray]
+  @{ML_response_fake [display,gray]
   "@{thm my_conjIa}
   |> Thm.proof_body_of
   |> get_names"
@@ -2037,7 +2040,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
@@ -2051,7 +2054,7 @@
   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
@@ -2064,7 +2067,7 @@
   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
@@ -2079,7 +2082,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 [display, gray]
+  @{ML_response_fake [display, gray]
   "@{thm my_conjIa}
   |> Thm.proof_body_of
   |> get_pbodies