diff -r b1a458a03a8e -r 74ba778b09c9 ProgTutorial/Parsing.thy
--- a/ProgTutorial/Parsing.thy	Sat Oct 31 11:37:41 2009 +0100
+++ b/ProgTutorial/Parsing.thy	Sun Nov 01 10:49:25 2009 +0100
@@ -82,8 +82,8 @@
 
   In the examples above we use the function @{ML_ind explode in Symbol} from the
   structure @{ML_struct Symbol}, instead of the more standard library function
-  @{ML_ind explode}, for obtaining an input list for the parser. The reason is
-  that @{ML_ind explode} in @{ML_struct Symbol} is aware of character
+  @{ML_ind explode in String}, for obtaining an input list for the parser. The reason is
+  that @{ML explode} in @{ML_struct Symbol} is aware of character
   sequences, for example @{text "\<foo>"}, that have a special meaning in
   Isabelle. To see the difference consider
 
@@ -780,7 +780,8 @@
   not yet used to type the variables: this must be done by type-inference later
   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_ind Mixfix} data structure;
+  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}.
 
   \begin{readmore}