src/Pure/ROOT
changeset 62665 a78ce0c6e191
parent 62585 5d4ed917450d
child 62666 00aff1da05ae
--- a/src/Pure/ROOT	Fri Mar 18 16:38:04 2016 +0100
+++ b/src/Pure/ROOT	Fri Mar 18 16:38:40 2016 +0100
@@ -101,7 +101,6 @@
     "ML/exn_debugger.ML"
     "ML/exn_properties.ML"
     "ML/fixed_int_dummy.ML"
-    "ML/install_pp_polyml.ML"
     "ML/ml_antiquotation.ML"
     "ML/ml_compiler.ML"
     "ML/ml_compiler0.ML"
@@ -113,6 +112,7 @@
     "ML/ml_lex.ML"
     "ML/ml_name_space.ML"
     "ML/ml_options.ML"
+    "ML/ml_pp.ML"
     "ML/ml_pretty.ML"
     "ML/ml_profiling.ML"
     "ML/ml_statistics.ML"