src/Pure/ML-Systems/polyml_common.ML
changeset 35010 d6e492cea6e4
parent 34136 3dcb46ae6185
child 35014 a725ff6ead26
--- a/src/Pure/ML-Systems/polyml_common.ML	Sat Feb 06 14:39:33 2010 +0100
+++ b/src/Pure/ML-Systems/polyml_common.ML	Sat Feb 06 14:50:55 2010 +0100
@@ -9,7 +9,7 @@
 use "ML-Systems/multithreading.ML";
 use "ML-Systems/time_limit.ML";
 use "ML-Systems/timing.ML";
-use "ML-Systems/system_shell.ML";
+use "ML-Systems/bash.ML";
 use "ML-Systems/ml_pretty.ML";
 use "ML-Systems/use_context.ML";