--- a/ProgTutorial/Essential.thy	Mon Jul 19 15:44:13 2010 +0100
+++ b/ProgTutorial/Essential.thy	Tue Jul 20 13:34:44 2010 +0100
@@ -1548,7 +1548,7 @@
   final statement of the theorem.
 
   @{ML_response_fake [display, gray]
-  "tracing (string_of_thm @{context} my_thm)"
+  "pwriteln (pretty_thm @{context} my_thm)"
   "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}
 
   However, internally the code-snippet constructs the following 
@@ -1769,8 +1769,8 @@
   @{ML_response_fake [display,gray,linenos]
   "Thm.reflexive @{cterm \"True\"}
   |> Simplifier.rewrite_rule [@{thm True_def}]
-  |> string_of_thm @{context}
-  |> tracing"
+  |> pretty_thm @{context}
+  |> pwriteln"
   "(\<lambda>x. x) = (\<lambda>x. x) \<equiv> (\<lambda>x. x) = (\<lambda>x. x)"}
 
   Often it is necessary to transform theorems to and from the object