diff -r c346c156a7cd -r a04bdee4fb1e CookBook/Parsing.thy
--- a/CookBook/Parsing.thy	Fri Nov 28 05:19:55 2008 +0100
+++ b/CookBook/Parsing.thy	Fri Nov 28 05:56:28 2008 +0100
@@ -45,7 +45,7 @@
   @{ML_response [display] "($$ \"h\") (explode \"hello\")" "(\"h\", [\"e\", \"l\", \"l\", \"o\"])"}
   @{ML_response [display] "($$ \"w\") (explode \"world\")" "(\"w\", [\"o\", \"r\", \"l\", \"d\"])"}
 
-  This function will either succeed (as in the two examples above) or raise the exeption 
+  This function will either succeed (as in the two examples above) or raise the exception 
   @{ML_text "FAIL"} if no string can be consumed. For example trying to parse
 
   @{ML_response_fake [display] "($$ \"x\") (explode \"world\")" 
@@ -68,7 +68,7 @@
   
   Slightly more general than the parser @{ML "(op $$)"} 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 prediate. For example the
+  one item from the input list satisfying this predicate. For example the
   following parser either consumes an @{ML_text [quotes] "h"} or a @{ML_text
   [quotes] "w"}:
 
@@ -83,7 +83,7 @@
 end"
     "((\"h\", [\"e\", \"l\", \"l\", \"o\"]),(\"w\", [\"o\", \"r\", \"l\", \"d\"]))"}
 
-  Two parser can be connected in sequence by using the funtion @{ML "(op --)"}. 
+  Two parser can be connected in sequence by using the function @{ML "(op --)"}. 
   For example parsing @{ML_text "h"}, @{ML_text "e"} and @{ML_text "l"} in this 
   sequence can be achieved by
 
@@ -107,7 +107,7 @@
 end"
   "((\"h\", [\"e\", \"l\", \"l\", \"o\"]), (\"w\", [\"o\", \"r\", \"l\", \"d\"]))"}
 
-  The functions @{ML "(op |--)"} and @{ML "(op --|)"} work like the sequencing funtion 
+  The functions @{ML "(op |--)"} and @{ML "(op --|)"} work like the sequencing function 
   for parsers, except that they discard the item being parsed by the first (respectively second)
   parser. For example
   
@@ -161,11 +161,11 @@
   which @{ML_text p} 
   is present in the input, but not @{ML_text q}. That means @{ML_open "(p -- q)" for p q} will fail 
   and the 
-  alternative parser @{ML_text r} will be tried. However in many circumstanes this will be the wrong
+  alternative parser @{ML_text r} will be tried. However in many 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 @{ML_text r}, not by the absense of @{ML_text q} in the input. This kind of situation
-  can be avoided by using the funtion @{ML "(op !!)"}. This function aborts the whole process of
+  failure of @{ML_text r}, not by the absence of @{ML_text q} in the input. This kind of situation
+  can be avoided by using the function @{ML "(op !!)"}. This function aborts the whole process of
   parsing in case of a failure and invokes an error message. For example if we invoke the parser
   
   @{ML [display] "(!! (fn _ => \"foo\") ($$ \"h\"))"}
@@ -333,7 +333,7 @@
  Token (\<dots>,(Keyword, \"|\"),\<dots>), 
  Token (\<dots>,(Keyword, \"for\"),\<dots>)]"}
 
-  we obtain a list consiting of only a command and two keyword tokens.
+  we obtain a list consisting of only a command and two keyword tokens.
   If you want to see which keywords and commands are currently known, use
   the following (you might have to adjust the @{ML print_depth} in order to
   see the complete list):