src/Pure/RAW/ROOT_polyml.ML
changeset 62359 6709e51d5c11
parent 62356 e307a410f46c
child 62387 ad3eb2889f9a
--- a/src/Pure/RAW/ROOT_polyml.ML	Wed Feb 17 23:29:35 2016 +0100
+++ b/src/Pure/RAW/ROOT_polyml.ML	Thu Feb 18 23:10:28 2016 +0100
@@ -75,7 +75,6 @@
 
 open Thread;
 use "RAW/multithreading.ML";
-use "RAW/multithreading_polyml.ML";
 
 if ML_System.name = "polyml-5.6"
 then use "RAW/ml_stack_polyml-5.6.ML"