diff -r e2b351efd6f3 -r d9a223c023f6 ProgTutorial/output_tutorial.ML
--- a/ProgTutorial/output_tutorial.ML	Wed Jun 02 10:08:16 2010 +0200
+++ b/ProgTutorial/output_tutorial.ML	Tue Jun 08 15:18:30 2010 +0200
@@ -2,7 +2,7 @@
 structure OutputTutorial =
 struct
 
-(* rebuilding the output function from ThyOutput in order to *)
+(* rebuilding the output function from Thy_Output in order to *)
 (* enable the options [gray, linenos]                        *)
 
 val gray = Unsynchronized.ref false
@@ -14,15 +14,15 @@
   val prts = map Pretty.str txt
 in   
   prts
-  |> (if ! ThyOutput.quotes then map Pretty.quote else I)
-  |> (if ! ThyOutput.display then
-    map (Output.output o Pretty.string_of o Pretty.indent (! ThyOutput.indent))
+  |> (if ! Thy_Output.quotes then map Pretty.quote else I)
+  |> (if ! Thy_Output.display then
+    map (Output.output o Pretty.string_of o Pretty.indent (! Thy_Output.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) 
     #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
   else
-    map (Output.output o (if ! ThyOutput.break then Pretty.string_of else Pretty.str_of))
+    map (Output.output o (if ! Thy_Output.break then Pretty.string_of else Pretty.str_of))
     #> space_implode "\\isasep\\isanewline%\n"
     #> enclose "\\isa{" "}")
 end
@@ -84,7 +84,7 @@
   | boolean "false" = false
   | boolean s = error ("Bad boolean value: " ^ quote s);
 
-val _ = ThyOutput.add_options
+val _ = Thy_Output.add_options
  [("gray", Library.setmp_CRITICAL gray o boolean),
   ("linenos", Library.setmp_CRITICAL linenos o boolean)]