--- a/src/Pure/General/print_mode.ML Sun Sep 16 14:59:10 2007 +0200
+++ b/src/Pure/General/print_mode.ML Sun Sep 16 15:27:26 2007 +0200
@@ -25,9 +25,8 @@
val print_mode = ref ([]: string list);
fun print_mode_active s = member (op =) (! print_mode) s;
-fun with_modes [] f x = f x
- | with_modes modes f x = NAMED_CRITICAL "print_mode" (fn () =>
- setmp print_mode (modes @ ! print_mode) f x);
+fun with_modes modes f x = NAMED_CRITICAL "print_mode" (fn () =>
+ setmp print_mode (modes @ ! print_mode) f x);
fun with_default f x = NAMED_CRITICAL "print_mode" (fn () =>
setmp print_mode [] f x);