--- a/CookBook/Parsing.thy	Sun Feb 08 08:45:25 2009 +0000
+++ b/CookBook/Parsing.thy	Mon Feb 09 01:12:00 2009 +0000
@@ -529,7 +529,7 @@
 
 text {*
   There are a number of special purpose parsers that help with parsing specifications
-  of functions, inductive definitions and so on. For example the function 
+  of functions, inductive definitions and so on. For example the 
   @{ML OuterParse.target} reads a target in order to indicate a locale.
 
 @{ML_response [display,gray]
@@ -543,9 +543,11 @@
   is wrapping the result into an option type and returning @{ML NONE} if no
   target is present.
 
-  The function @{ML OuterParse.fixes} reads a list of constants
-  that can include type annotations and syntax translations.
-  The list is separated by \isacommand{and}. For example:
+  The function @{ML OuterParse.fixes} reads an \isacommand{and}-separated 
+  list of constants that can include type annotations and syntax translations. 
+  For example:\footnote{Note that in the code we need to write 
+  @{text "\\\"int \<Rightarrow> bool\\\""} in order to properly escape the double quotes
+  in the compound type.}
 *}
 
 text {*
@@ -561,9 +563,12 @@
   (bar, SOME \<dots>, NoSyn), 
   (blonk, NONE, NoSyn)],[])"}  
 
-  Whenever types are given, then they are stored in the @{ML SOME}s. 
-  Note that we had to write @{text "\\\"int \<Rightarrow> bool\\\""} to properly escape 
-  the double quotes in the compound type.
+  Whenever types are given, then they are stored in the @{ML SOME}s.
+  If a syntax translation is present for a constant, then it is
+  stored in the @{ML Mixfix} data structure; no syntax translation is
+  indicated by @{ML NoSyn}.
+ 
+  (FIXME: should for-fixes take any syntax annotation?)
 
   @{ML OuterParse.for_fixes} is an ``optional'' that prefixes 
   @{ML OuterParse.fixes} with the comman \isacommand{for}.