--- a/src/Pure/ML-Systems/polyml-5.1.ML Sun Sep 07 17:46:44 2008 +0200 +++ b/src/Pure/ML-Systems/polyml-5.1.ML Sun Sep 07 17:48:49 2008 +0200 @@ -10,4 +10,3 @@ use "ML-Systems/polyml_old_compiler5.ML"; val pointer_eq = PolyML.pointerEq; -