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