diff -r 796c6ea633b3 -r 5f003fdf2653 CookBook/chunks.ML
--- a/CookBook/chunks.ML	Sat Feb 14 00:24:05 2009 +0000
+++ b/CookBook/chunks.ML	Sat Feb 14 13:20:21 2009 +0000
@@ -20,8 +20,8 @@
   |> (if ! ThyOutput.display then
     map (Output.output o Pretty.string_of o Pretty.indent (! ThyOutput.indent))
     #> space_implode "\\isasep\\isanewline%\n"
+    #> (if ! linenos then (enclose "\\begin{linenos}%\n" "%\n\\end{linenos}") else I) 
     #> (if ! gray then (enclose "\\begin{graybox}%\n" "%\n\\end{graybox}") else I) 
-    #> (if ! linenos then (enclose "\\begin{linenos}%\n" "%\n\\end{linenos}") else I) 
     #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
  else
     map (Output.output o (if ! ThyOutput.break then Pretty.string_of else Pretty.str_of))