--- a/CookBook/Parsing.thy	Mon Feb 09 04:18:14 2009 +0000
+++ b/CookBook/Parsing.thy	Wed Feb 11 17:40:24 2009 +0000
@@ -37,7 +37,7 @@
 text {*
 
   Let us first have a look at parsing strings using generic parsing combinators. 
-  The function @{ML "(op $$)"} takes a string as argument and will ``consume'' this string from 
+  The function @{ML "$$"} takes a string as argument and will ``consume'' this string from 
   a given input list of strings. ``Consume'' in this context means that it will 
   return a pair consisting of this string and the rest of the input list. 
   For example:
@@ -61,13 +61,13 @@
   \item @{text "MORE"} indicates that there is not enough input for the parser. For example 
   in @{text "($$ \"h\") []"}.
   \item @{text "ABORT"} is the exception that is raised when a dead end is reached. 
-  It is used for example in the function @{ML "(op !!)"} (see below).
+  It is used for example in the function @{ML "!!"} (see below).
   \end{itemize}
 
   However, note that these exceptions are private to the parser and cannot be accessed
   by the programmer (for example to handle them).
   
-  Slightly more general than the parser @{ML "(op $$)"} is the function @{ML
+  Slightly more general than the parser @{ML "$$"} is the function @{ML
   Scan.one}, in that it takes a predicate as argument and then parses exactly
   one item from the input list satisfying this predicate. For example the
   following parser either consumes an @{text [quotes] "h"} or a @{text
@@ -84,7 +84,7 @@
 end"
     "((\"h\", [\"e\", \"l\", \"l\", \"o\"]),(\"w\", [\"o\", \"r\", \"l\", \"d\"]))"}
 
-  Two parser can be connected in sequence by using the function @{ML "(op --)"}. 
+  Two parser can be connected in sequence by using the function @{ML "--"}. 
   For example parsing @{text "h"}, @{text "e"} and @{text "l"} in this 
   sequence you can achieve by:
 
@@ -100,7 +100,7 @@
                           "(\"hell\", [\"o\"])"}
 
   Parsers that explore alternatives can be constructed using the function @{ML
-  "(op ||)"}. For example, the parser @{ML "(p || q)" for p q} returns the
+  "||"}. For example, the parser @{ML "(p || q)" for p q} returns the
   result of @{text "p"}, in case it succeeds, otherwise it returns the
   result of @{text "q"}. For example:
 
@@ -115,7 +115,7 @@
 end"
   "((\"h\", [\"e\", \"l\", \"l\", \"o\"]), (\"w\", [\"o\", \"r\", \"l\", \"d\"]))"}
 
-  The functions @{ML "(op |--)"} and @{ML "(op --|)"} work like the sequencing function 
+  The functions @{ML "|--"} and @{ML "--|"} work like the sequencing function 
   for parsers, except that they discard the item being parsed by the first (respectively second)
   parser. For example:
   
@@ -155,7 +155,7 @@
   (p input1, p input2)
 end" "((SOME \"h\", [\"e\", \"l\", \"l\", \"o\"]), (NONE, [\"w\", \"o\", \"r\", \"l\", \"d\"]))"}
 
-  The function @{ML "(op !!)"} helps to produce appropriate error messages
+  The function @{ML "!!"} helps to produce appropriate error messages
   during parsing. For example if you want to parse that @{text p} is immediately 
   followed by @{text q}, or start a completely different parser @{text r},
   you might write:
@@ -171,7 +171,7 @@
   circumstance this will be the wrong parser for the input ``p-followed-by-q''
   and therefore will also fail. The error message is then caused by the
   failure of @{text r}, not by the absence of @{text q} in the input. This
-  kind of situation can be avoided when using the function @{ML "(op !!)"}. 
+  kind of situation can be avoided when using the function @{ML "!!"}. 
   This function aborts the whole process of parsing in case of a
   failure and prints an error message. For example if you invoke the parser
 
@@ -189,7 +189,7 @@
   @{ML_response_fake [display,gray] "(!! (fn _ => \"foo\") ($$ \"h\")) (explode \"world\")"
                                "Exception ABORT raised"}
 
-  then the parsing aborts and the error message @{text "foo"} is printed out. In order to
+  then the parsing aborts and the error message @{text "foo"} is printed. In order to
   see the error message properly, we need to prefix the parser with the function 
   @{ML "Scan.error"}. For example:
 
@@ -430,7 +430,7 @@
 end"
 "((\"where\",\<dots>),(\"|\",\<dots>))"}
 
-  Like before, you can sequentially connect parsers with @{ML "(op --)"}. For example: 
+  Like before, you can sequentially connect parsers with @{ML "--"}. For example: 
 
 @{ML_response [display,gray]
 "let 
@@ -571,7 +571,7 @@
   (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}.
+  @{ML OuterParse.fixes} with the command \isacommand{for}.
   (FIXME give an example and explain more)
 
 @{ML_response [display,gray]