diff -r 4a1539a2c18e -r d84867127c5d ProgTutorial/First_Steps.thy
--- a/ProgTutorial/First_Steps.thy	Fri May 17 11:01:55 2013 +0100
+++ b/ProgTutorial/First_Steps.thy	Tue May 28 23:26:18 2013 +0100
@@ -166,22 +166,7 @@
   "(1::nat, x::'a)"}
 
   where @{text 1} and @{text x} are displayed with their inferred type.
-  Even more type information can be printed by setting 
-  the reference @{ML_ind show_all_types in Syntax} to @{ML true}. 
-  In this case we obtain
-*}
-
-text {*
-  @{ML_response_fake [display, gray]
-  "let 
-  val show_all_types_ctxt = Config.put show_all_types true @{context}
-in
-  pwriteln (pretty_term show_all_types_ctxt @{term \"(1::nat, x)\"})
-end"
-  "(Pair::nat \<Rightarrow> 'a \<Rightarrow> nat \<times> 'a) (1::nat) (x::'a)"}
-
-  where now even @{term Pair} is written with its type (@{term Pair} is the
-  term-constructor for products). Other configuration values that influence
+  Other configuration values that influence
   printing of terms include 
 
   \begin{itemize}