# HG changeset patch
# User wenzelm
# Date 1117729794 -7200
# Node ID 3d192ab9907b42a16daf7b0dda9f4d463e8d355a
# Parent  05413e43d2f3fe0b68f7f3b148b90d6b885c8378
Output.no_warnings;

diff -r 05413e43d2f3 -r 3d192ab9907b src/Pure/Isar/isar_output.ML
--- a/src/Pure/Isar/isar_output.ML	Thu Jun 02 18:29:53 2005 +0200
+++ b/src/Pure/Isar/isar_output.ML	Thu Jun 02 18:29:54 2005 +0200
@@ -37,8 +37,6 @@
 structure T = OuterLex;
 structure P = OuterParse;
 
-
-
 (** global references -- defaults for options **)
 
 val locale = ref "";
@@ -168,7 +166,7 @@
           let val (opts, src) = antiq_args lex x in
             options opts (fn () => command src state) ();  (*preview errors!*)
             Library.setmp print_mode (! modes @ Latex.modes @ ! print_mode)
-              (options opts (fn () => command src state)) ()
+              (Output.no_warnings (options opts (fn () => command src state))) ()
           end;
     val ants = Antiquote.antiquotes_of (str, pos);
   in