
diff -r 0c3580c831a4 -r 1783211b3494 CookBook/Parsing.thy
--- a/CookBook/Parsing.thy	Sat Nov 29 21:20:18 2008 +0000
+++ b/CookBook/Parsing.thy	Sat Dec 13 01:33:22 2008 +0000
@@ -399,7 +399,7 @@
 end" 
 "([\"in\",\"in\",\"in\"],[])"}
 
-  The following function will help us to run examples
+  The following function will help us later to run examples
 
 *}
 
@@ -427,8 +427,8 @@
 
   \begin{exercise}
   A type-identifier, for example @{typ "'a"}, is a token of 
-  kind @{ML "Keyword" in OuterLex} can be parsed 
-
+  kind @{ML "Keyword" in OuterLex}. It can be parsed using 
+  the function @{ML OuterParse.type_ident}.
   \end{exercise}
 
 




