# HG changeset patch
# User wenzelm
# Date 954961293 -7200
# Node ID ee73e7b2668629fe40d5d0f7761d927b70313d43
# Parent  4230d17073eac455b881f5b0a3ca83a1bf7e2dc1
suppress warning;

diff -r 4230d17073ea -r ee73e7b26686 src/Pure/Interface/proof_general.ML
--- a/src/Pure/Interface/proof_general.ML	Tue Apr 04 22:16:11 2000 +0200
+++ b/src/Pure/Interface/proof_general.ML	Wed Apr 05 21:01:33 2000 +0200
@@ -247,7 +247,7 @@
 (* init *)
 
 fun init isar =
- (if isar then init_outer_syntax () else ();
+ (if isar then setmp warning_fn (K ()) init_outer_syntax () else ();
   setup_xsymbols_output ();
   setup_messages ();
   setup_state ();