diff -r 2c34c69236ce -r 3c214b215f7e ProgTutorial/Parsing.thy
--- a/ProgTutorial/Parsing.thy	Sun Apr 06 12:45:54 2014 +0100
+++ b/ProgTutorial/Parsing.thy	Wed May 28 12:41:09 2014 +0100
@@ -1,5 +1,7 @@
 theory Parsing
-imports Base "Helper/Command/Command" "Package/Simple_Inductive_Package"
+imports Base "Package/Simple_Inductive_Package"
+keywords "foobar" "foobar_trace" :: thy_decl and
+         "foobar_goal" "foobar_prove" :: thy_goal
 begin
 
 chapter {* Parsing\label{chp:parsing} *}
@@ -71,8 +73,10 @@
   "($$ \"x\") (Symbol.explode \"world\")" 
   "Exception FAIL raised"}
   
-  will raise the exception @{text "FAIL"}.  There are three exceptions used in
-  the parsing combinators:
+  will raise the exception @{text "FAIL"}. The function @{ML_ind "$$" in Scan} will also
+  fail if you try to consume more than a single character.
+
+  There are three exceptions that are raised by the parsing combinators:
 
   \begin{itemize}
   \item @{text "FAIL"} is used to indicate that alternative routes of parsing 
@@ -223,8 +227,7 @@
 
 
   @{ML [display,gray] "!! (fn _ => fn _ =>\"foo\") ($$ \"h\")"}
-*}
-text {*
+
   on @{text [quotes] "hello"}, the parsing succeeds
 
   @{ML_response [display,gray] 
@@ -241,10 +244,11 @@
   @{ML_ind error in Scan}. For example:
 
   @{ML_response_fake [display,gray] 
-  "Scan.error (!! (fn _ => fn _ => \"foo\") ($$ \"h\"))"
+  "Scan.error (!! (fn _ => fn _ => \"foo\") ($$ \"h\")) (Symbol.explode \"world\")"
   "Exception Error \"foo\" raised"}
 
-  This ``prefixing'' is usually done by wrappers such as @{ML_ind local_theory in Outer_Syntax} 
+  This kind of ``prefixing'' to see the correct error message is usually done by wrappers 
+  such as @{ML_ind local_theory in Outer_Syntax} 
   (see Section~\ref{sec:newcommand} which explains this function in more detail). 
   
   Let us now return to our example of parsing @{ML "(p -- q) || r" for p q