diff -r 01aa36932739 -r f652333bbf8e src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Thu May 27 17:41:27 2010 +0200
+++ b/src/Pure/Thy/thy_output.ML	Thu May 27 18:10:37 2010 +0200
@@ -153,7 +153,7 @@
       | expand (Antiquote.Antiq (ss, (pos, _))) =
           let val (opts, src) = Token.read_antiq lex antiq (ss, pos) in
             options opts (fn () => command src state) ();  (*preview errors!*)
-            PrintMode.with_modes (! modes @ Latex.modes)
+            Print_Mode.with_modes (! modes @ Latex.modes)
               (Output.no_warnings_CRITICAL (options opts (fn () => command src state))) ()
           end
       | expand (Antiquote.Open _) = ""
@@ -429,7 +429,7 @@
   ("display", setmp_CRITICAL display o boolean),
   ("break", setmp_CRITICAL break o boolean),
   ("quotes", setmp_CRITICAL quotes o boolean),
-  ("mode", fn s => fn f => PrintMode.with_modes [s] f),
+  ("mode", fn s => fn f => Print_Mode.with_modes [s] f),
   ("margin", setmp_CRITICAL Pretty.margin_default o integer),
   ("indent", setmp_CRITICAL indent o integer),
   ("source", setmp_CRITICAL source o boolean),