# HG changeset patch
# User wenzelm
# Date 1282937011 -7200
# Node ID 52cee2c5f219fc253a4a66b11f4649a3f83411ff
# Parent  088502dfd89f561947c05a798139ca2966c0f5f6
discontinued broken no_warnings_CRITICAL -- global output channels must not be changed after startup initialization;

diff -r 088502dfd89f -r 52cee2c5f219 src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Fri Aug 27 21:22:07 2010 +0200
+++ b/src/Pure/General/output.ML	Fri Aug 27 21:23:31 2010 +0200
@@ -45,7 +45,6 @@
   val status: string -> unit
   val report: string -> unit
   val debugging: bool Unsynchronized.ref
-  val no_warnings_CRITICAL: ('a -> 'b) -> 'a -> 'b
   val debug: (unit -> string) -> unit
 end;
 
@@ -113,8 +112,6 @@
 
 fun legacy_feature s = warning ("Legacy feature! " ^ s);
 
-fun no_warnings_CRITICAL f = setmp_CRITICAL warning_fn (K ()) f;
-
 val debugging = Unsynchronized.ref false;
 fun debug s = if ! debugging then ! debug_fn (output (s ())) else ()