diff -r 2494b5b7a85d -r e6f583366779 ProgTutorial/Parsing.thy
--- a/ProgTutorial/Parsing.thy	Mon Nov 02 12:47:00 2009 +0100
+++ b/ProgTutorial/Parsing.thy	Mon Nov 02 16:26:03 2009 +0100
@@ -781,11 +781,11 @@
   on. Since types are part of the inner syntax they are strings with some
   encoded information (see previous section). If a mixfix-syntax is
   present for a variable, then it is stored in the 
-  @{ML Mixfix}\footnote{FIXME: access to Mixfix data structure} data structure;
-  no syntax translation is indicated by @{ML_ind NoSyn}.
+  @{ML Mixfix} data structure; no syntax translation is indicated by @{ML_ind NoSyn in Syntax}.
 
   \begin{readmore}
-  The data structure for mixfix annotations is defined in @{ML_file "Pure/Syntax/mixfix.ML"}.
+  The data structure for mixfix annotations are implemented in 
+  @{ML_file "Pure/Syntax/mixfix.ML"} and @{ML_file "Pure/Syntax/syntax.ML"}.
   \end{readmore}
 
   Lines 3 to 7 in the function @{ML spec_parser} implement the parser for a