diff -r 9b6c9d172378 -r 13fd0a83d3c3 CookBook/Parsing.thy --- a/CookBook/Parsing.thy Fri Feb 13 01:05:31 2009 +0000 +++ b/CookBook/Parsing.thy Fri Feb 13 09:57:08 2009 +0000 @@ -834,7 +834,7 @@ we set the kind indicator to @{ML thy_goal in OuterKeyword}. *} -ML%linenumbers{*let +ML%linenosgray{*let fun set_up_thm str ctxt = let val prop = Syntax.read_prop ctxt str