--- 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}