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}