--- a/ProgTutorial/FirstSteps.thy	Sun Nov 01 10:49:25 2009 +0100
+++ b/ProgTutorial/FirstSteps.thy	Mon Nov 02 12:47:00 2009 +0100
@@ -254,6 +254,38 @@
   commas (map (string_of_term ctxt) ts)*}
 
 text {*
+  Sometimes you want to print out a term together with some type information.
+  This can be achieved by setting the reference 
+  @{ML_ind show_types}\footnote{\bf FIXME: ``forgotten'' structure Printer, Mixfix etc.} 
+  to @{ML true}.
+*}
+
+ML{*show_types := true*}
+
+text {*
+  Now @{ML string_of_term} prints out
+
+  @{ML_response_fake [display, gray]
+  "tracing (string_of_term @{context} @{term \"(1::nat, x)\"})"
+  "(1::nat, x::'a)"}
+
+  where @{text 1} and @{text x} are displayed with their type.
+  Even more type information can be printed by setting 
+  @{ML_ind show_all_types} to @{ML true}. We obtain
+*}
+(*<*)ML %linenos {*show_all_types := true*}
+(*>*)
+text {*
+  @{ML_response_fake [display, gray]
+  "tracing (string_of_term @{context} @{term \"(1::nat, x)\"})"
+  "(Pair::nat \<Rightarrow> 'a \<Rightarrow> nat \<times> 'a) (1::nat) (x::'a)"}
+
+  Other references that influence printing are @{ML_ind show_brackets} 
+  and @{ML_ind show_sorts}. 
+*}
+(*<*)ML %linenos {*show_types := false; show_all_types := false*}
+(*>*)
+text {*
   A @{ML_type cterm} can be transformed into a string by the following function.
 *}
 
@@ -321,6 +353,13 @@
   commas (map (string_of_thm_no_vars ctxt) thms) *}
 
 text {*
+  \begin{readmore}
+  The simple conversion functions from Isabelle's main datatypes to 
+  @{ML_type string}s are implemented in @{ML_file "Pure/Syntax/syntax.ML"}. 
+  The references that change the printing information are declared in 
+  @{ML_file "Pure/Syntax/printer.ML"}.
+  \end{readmore}
+
   Note that when printing out several ``parcels'' of information that
   semantically belong together, like a warning message consisting of 
   a term and its type, you should try to keep this information together in a
@@ -1303,7 +1342,7 @@
 
   \begin{conventions}
   \begin{itemize}
-  \item Print messages that belong together as a single string.
+  \item Print messages that belong together in a single string.
   \item Do not use references in Isabelle code.
   \end{itemize}
   \end{conventions}