diff -r 01aa36932739 -r f652333bbf8e src/Pure/General/print_mode.ML
--- a/src/Pure/General/print_mode.ML	Thu May 27 17:41:27 2010 +0200
+++ b/src/Pure/General/print_mode.ML	Thu May 27 18:10:37 2010 +0200
@@ -22,7 +22,7 @@
   val closure: ('a -> 'b) -> 'a -> 'b
 end;
 
-structure PrintMode: PRINT_MODE =
+structure Print_Mode: PRINT_MODE =
 struct
 
 val input = "input";
@@ -49,5 +49,5 @@
 
 end;
 
-structure BasicPrintMode: BASIC_PRINT_MODE = PrintMode;
-open BasicPrintMode;
+structure Basic_Print_Mode: BASIC_PRINT_MODE = Print_Mode;
+open Basic_Print_Mode;