diff -r f65b9f14d5de -r 1bbe4268664d ProgTutorial/Parsing.thy
--- a/ProgTutorial/Parsing.thy	Tue Jun 28 09:22:00 2011 +0100
+++ b/ProgTutorial/Parsing.thy	Sun Jul 31 00:00:58 2011 +0100
@@ -222,18 +222,19 @@
   aborts the whole process of parsing in case of a failure and prints an error
   message. For example if you invoke the parser
 
-  
-  @{ML [display,gray] "!! (fn _ => \"foo\") ($$ \"h\")"}
 
+  @{ML [display,gray] "!! (fn _ => fn _ =>\"foo\") ($$ \"h\")"}
+*}
+text {*
   on @{text [quotes] "hello"}, the parsing succeeds
 
   @{ML_response [display,gray] 
-  "(!! (fn _ => \"foo\") ($$ \"h\")) (Symbol.explode \"hello\")" 
+  "(!! (fn _ => fn _ => \"foo\") ($$ \"h\")) (Symbol.explode \"hello\")" 
   "(\"h\", [\"e\", \"l\", \"l\", \"o\"])"}
 
   but if you invoke it on @{text [quotes] "world"}
-  
-  @{ML_response_fake [display,gray] "(!! (fn _ => \"foo\") ($$ \"h\")) (Symbol.explode \"world\")"
+
+  @{ML_response_fake [display,gray] "(!! (fn _ => fn _ => \"foo\") ($$ \"h\")) (Symbol.explode \"world\")"
                                "Exception ABORT raised"}
 
   then the parsing aborts and the error message @{text "foo"} is printed. In order to
@@ -241,7 +242,7 @@
   @{ML_ind error in Scan}. For example:
 
   @{ML_response_fake [display,gray] 
-  "Scan.error (!! (fn _ => \"foo\") ($$ \"h\"))"
+  "Scan.error (!! (fn _ => fn _ => \"foo\") ($$ \"h\"))"
   "Exception Error \"foo\" raised"}
 
   This ``prefixing'' is usually done by wrappers such as @{ML_ind local_theory in Outer_Syntax} 
@@ -256,7 +257,7 @@
 let 
   val err_msg = fn _ => p ^ " is not followed by " ^ q
 in
-  ($$ p -- (!! err_msg ($$ q))) || ($$ r -- $$ r)
+  ($$ p -- (!! (fn _ => err_msg) ($$ q))) || ($$ r -- $$ r)
 end *}