suppress warning;
authorwenzelm
Wed, 05 Apr 2000 21:01:33 +0200
changeset 8668 ee73e7b26686
parent 8667 4230d17073ea
child 8669 3ccb29fb26ef
suppress warning;
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 ();