# HG changeset patch
# User wenzelm
# Date 975696220 -3600
# Node ID fc7afc98a329a52cef6cf3daca0702561fe92a36
# Parent  e8346dad78e1d5201fff701fb830dc83319fb019
append print_modes;

diff -r e8346dad78e1 -r fc7afc98a329 src/Pure/Isar/isar_output.ML
--- a/src/Pure/Isar/isar_output.ML	Fri Dec 01 19:43:06 2000 +0100
+++ b/src/Pure/Isar/isar_output.ML	Fri Dec 01 19:43:40 2000 +0100
@@ -141,7 +141,8 @@
     fun expand (Antiquote.Text s) = s
       | expand (Antiquote.Antiq x) =
           let val (opts, src) = antiq_args lex x in
-            Library.setmp print_mode Latex.modes (options opts (fn () => command src state)) ()
+            Library.setmp print_mode (Latex.modes @ ! print_mode)
+              (options opts (fn () => command src state)) ()
           end;
     val ants = Antiquote.antiquotes_of (str, pos);
   in