src/Pure/pure_setup.ML
changeset 38327 d6afb77b0f6d
parent 37954 a2e73df0b1e0
child 38470 484e483eb606
--- a/src/Pure/pure_setup.ML	Wed Aug 11 12:50:33 2010 +0200
+++ b/src/Pure/pure_setup.ML	Wed Aug 11 13:39:36 2010 +0200
@@ -40,9 +40,9 @@
 toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract";
 
 if ml_system = "polyml-5.3.0"
-then use "ML-Systems/install_pp_polyml-5.3.ML"
+then use "ML/install_pp_polyml-5.3.ML"
 else if String.isPrefix "polyml" ml_system
-then use "ML-Systems/install_pp_polyml.ML"
+then use "ML/install_pp_polyml.ML"
 else ();
 
 if ml_system = "polyml-5.0" orelse ml_system = "polyml-5.1" then