--- a/ProgTutorial/FirstSteps.thy	Mon Nov 02 12:47:00 2009 +0100
+++ b/ProgTutorial/FirstSteps.thy	Mon Nov 02 16:26:03 2009 +0100
@@ -255,8 +255,7 @@
 
 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.} 
+  This can be achieved by setting the reference @{ML_ind show_types in Syntax} 
   to @{ML true}.
 *}
 
@@ -271,7 +270,7 @@
 
   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_ind show_all_types in Syntax} to @{ML true}. We obtain
 *}
 (*<*)ML %linenos {*show_all_types := true*}
 (*>*)
@@ -280,8 +279,8 @@
   "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}. 
+  Other references that influence printing are @{ML_ind show_brackets in Syntax} 
+  and @{ML_ind show_sorts in Syntax}. 
 *}
 (*<*)ML %linenos {*show_types := false; show_all_types := false*}
 (*>*)