src/Pure/General/print_mode.ML
changeset 37146 f652333bbf8e
parent 33223 d27956b4d3b4
child 39124 9bac2f4cfd6e
     1.1 --- a/src/Pure/General/print_mode.ML	Thu May 27 17:41:27 2010 +0200
     1.2 +++ b/src/Pure/General/print_mode.ML	Thu May 27 18:10:37 2010 +0200
     1.3 @@ -22,7 +22,7 @@
     1.4    val closure: ('a -> 'b) -> 'a -> 'b
     1.5  end;
     1.6  
     1.7 -structure PrintMode: PRINT_MODE =
     1.8 +structure Print_Mode: PRINT_MODE =
     1.9  struct
    1.10  
    1.11  val input = "input";
    1.12 @@ -49,5 +49,5 @@
    1.13  
    1.14  end;
    1.15  
    1.16 -structure BasicPrintMode: BASIC_PRINT_MODE = PrintMode;
    1.17 -open BasicPrintMode;
    1.18 +structure Basic_Print_Mode: BASIC_PRINT_MODE = Print_Mode;
    1.19 +open Basic_Print_Mode;