diff -r b83c75d051b7 -r a0b280dd4bc7 ProgTutorial/Essential.thy --- 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)" "\\x. P x \ Q x; P t\ \ 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" "(\x. x) = (\x. x) \ (\x. x) = (\x. x)"} Often it is necessary to transform theorems to and from the object