diff -r edee1966fddf -r b27b7c2200b9 src/Pure/General/print_mode.ML
--- a/src/Pure/General/print_mode.ML	Mon Mar 07 08:14:18 2016 +0100
+++ b/src/Pure/General/print_mode.ML	Mon Mar 07 09:49:58 2016 +0100
@@ -23,6 +23,7 @@
   val setmp: string list -> ('a -> 'b) -> 'a -> 'b
   val with_modes: string list -> ('a -> 'b) -> 'a -> 'b
   val closure: ('a -> 'b) -> 'a -> 'b
+  val add_modes: string list -> unit
 end;
 
 structure Print_Mode: PRINT_MODE =
@@ -51,6 +52,8 @@
 fun with_modes modes f x = setmp (modes @ print_mode_value ()) f x;
 fun closure f = with_modes [] f;
 
+fun add_modes modes = Unsynchronized.change print_mode (append modes);
+
 end;
 
 structure Basic_Print_Mode: BASIC_PRINT_MODE = Print_Mode;