src/Pure/ROOT.ML
changeset 62665 a78ce0c6e191
parent 62662 291cc01f56f5
child 62666 00aff1da05ae
     1.1 --- a/src/Pure/ROOT.ML	Fri Mar 18 16:38:04 2016 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Fri Mar 18 16:38:40 2016 +0100
     1.3 @@ -393,8 +393,7 @@
     1.4  
     1.5  structure Output: OUTPUT = Output;  (*seal system channels!*)
     1.6  
     1.7 -
     1.8 -use "ML/install_pp_polyml.ML";
     1.9 +use "ML/ml_pp.ML";
    1.10  
    1.11  
    1.12  (* the Pure theory *)