src/Pure/codegen.ML
changeset 37146 f652333bbf8e
parent 36953 2af1ad9aa1a3
child 37198 3af985b10550
     1.1 --- a/src/Pure/codegen.ML	Thu May 27 17:41:27 2010 +0200
     1.2 +++ b/src/Pure/codegen.ML	Thu May 27 18:10:37 2010 +0200
     1.3 @@ -109,9 +109,9 @@
     1.4  
     1.5  val margin = Unsynchronized.ref 80;
     1.6  
     1.7 -fun string_of p = PrintMode.setmp [] (Pretty.string_of_margin (!margin)) p;
     1.8 +fun string_of p = Print_Mode.setmp [] (Pretty.string_of_margin (!margin)) p;
     1.9  
    1.10 -val str = PrintMode.setmp [] Pretty.str;
    1.11 +val str = Print_Mode.setmp [] Pretty.str;
    1.12  
    1.13  (**** Mixfix syntax ****)
    1.14