src/Pure/General/print_mode.ML
changeset 33223 d27956b4d3b4
parent 32738 15bb09ca0378
child 37146 f652333bbf8e
     1.1 --- a/src/Pure/General/print_mode.ML	Tue Oct 27 13:15:20 2009 +0100
     1.2 +++ b/src/Pure/General/print_mode.ML	Tue Oct 27 13:16:16 2009 +0100
     1.3 @@ -35,7 +35,7 @@
     1.4    let val modes =
     1.5      (case Thread.getLocal tag of
     1.6        SOME (SOME modes) => modes
     1.7 -    | _ => NAMED_CRITICAL "print_mode" (fn () => ! print_mode))
     1.8 +    | _ => ! print_mode)
     1.9    in subtract (op =) [input, internal] modes end;
    1.10  
    1.11  fun print_mode_active mode = member (op =) (print_mode_value ()) mode;