src/Pure/ML-Systems/smlnj.ML
changeset 16528 25a7459d4d4a
parent 16502 5a56e59526a5
child 16542 1259088dc448
--- a/src/Pure/ML-Systems/smlnj.ML	Wed Jun 22 11:09:14 2005 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Wed Jun 22 11:20:45 2005 +0200
@@ -13,9 +13,13 @@
 
 (* low-level pointer equality *)
 
-(*proper implementation available?*)
+(*proper implementation available? This declaration may get overridden below.*)
 fun pointer_eq (x:''a, y) = false;
 
+(case #version_id (Compiler.version) of
+  [110, x] => if x >= 49 then use "ML-Systems/smlnj-ptreql.ML" else ()
+| _ => ());
+
 
 (* restore old-style character / string functions *)