CookBook/Recipes/Antiquotes.thy
changeset 114 13fd0a83d3c3
parent 74 f6f8f8ba1eb1
child 153 c22b507e1407
--- a/CookBook/Recipes/Antiquotes.thy	Fri Feb 13 01:05:31 2009 +0000
+++ b/CookBook/Recipes/Antiquotes.thy	Fri Feb 13 09:57:08 2009 +0000
@@ -33,7 +33,7 @@
 
 *}
 
-ML%linenumbers{*fun ml_val code_txt = "val _ = " ^ code_txt
+ML%linenosgray{*fun ml_val code_txt = "val _ = " ^ code_txt
 
 fun output_ml src ctxt code_txt =
   (ML_Context.eval_in (SOME ctxt) false Position.none (ml_val code_txt); 
@@ -67,7 +67,7 @@
   can improve the code above slightly by writing 
 *}
 
-ML%linenumbers{*fun output_ml src ctxt (code_txt,pos) =
+ML%linenosgray{*fun output_ml src ctxt (code_txt,pos) =
   (ML_Context.eval_in (SOME ctxt) false pos (ml_val code_txt);
   ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt 
                                             (space_explode "\n" code_txt))