diff -r 7235374f34c8 -r 018bfa718982 CookBook/chunks.ML
--- a/CookBook/chunks.ML	Wed Feb 04 20:26:38 2009 +0000
+++ b/CookBook/chunks.ML	Thu Feb 05 16:34:05 2009 +0000
@@ -26,9 +26,14 @@
     #> space_implode "\\isasep\\isanewline%\n"
     #> enclose "\\isa{" "}");
 
+fun output pretty src ctxt = output_list pretty src ctxt o single
+
 val _ = ThyOutput.add_options
  [("gray", Library.setmp gray o boolean)]
 
+
+
+
 (** theory data **)
 
 structure ChunkData = TheoryDataFun