--- a/src/Pure/IsaMakefile Wed Jun 22 11:09:14 2005 +0200
+++ b/src/Pure/IsaMakefile Wed Jun 22 11:20:45 2005 +0200
@@ -47,7 +47,7 @@
ML-Systems/polyml-time-limit.ML ML-Systems/polyml.ML \
ML-Systems/polyml-posix.ML \
ML-Systems/smlnj-basis-compat.ML ML-Systems/smlnj-compiler.ML \
- ML-Systems/smlnj-pp-new.ML ML-Systems/smlnj-pp-old.ML \
+ ML-Systems/smlnj-ptreql.ML ML-Systems/smlnj-pp-new.ML ML-Systems/smlnj-pp-old.ML \
ML-Systems/smlnj.ML Proof/extraction.ML Proof/proof_rewrite_rules.ML \
Proof/proof_syntax.ML Proof/proofchecker.ML Proof/reconstruct.ML \
Pure.thy ROOT.ML Syntax/ROOT.ML Syntax/ast.ML Syntax/lexicon.ML \
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/smlnj-ptreql.ML Wed Jun 22 11:20:45 2005 +0200
@@ -0,0 +1,10 @@
+(* Title: $Id$
+ Author: Lawrence C Paulson
+
+Pointer Equality: for Standard ML of New Jersey 110.49 or later.
+
+Thanks to Matthias Blume for providing InlineT.ptreql!
+*)
+
+CM.autoload "$smlnj/init/init.cmi";
+val pointer_eq = InlineT.ptreql;
--- 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 *)