use polyml_old_compiler5.ML;

--- a/src/Pure/ML-Systems/polyml-5.1.ML	Tue Mar 25 08:29:50 2008 +0100
+++ b/src/Pure/ML-Systems/polyml-5.1.ML	Tue Mar 25 11:52:15 2008 +0100
@@ -6,6 +6,7 @@
 
 use "ML-Systems/polyml_common.ML";
 use "ML-Systems/multithreading_polyml.ML";
+use "ML-Systems/polyml_old_compiler5.ML";
 
 val pointer_eq = PolyML.pointerEq;
 
@@ -18,4 +19,3 @@
   | profile n f x = NAMED_CRITICAL "profile" (fn () => profile_orig n f x);
 
 end;
-