CookBook/Parsing.thy
changeset 114 13fd0a83d3c3
parent 108 8bea3f74889d
child 116 c9ff326e3ce5
--- 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