# HG changeset patch
# User wenzelm
# Date 1206442335 -3600
# Node ID 3835c431e1410cd81eecd0ee810af2d026935c38
# Parent  b879f68cf92b81f9fe31d0a9e68bdefb6fe30cdf
use polyml_old_compiler5.ML;

diff -r b879f68cf92b -r 3835c431e141 src/Pure/ML-Systems/polyml-5.1.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;
-