# HG changeset patch
# User paulson
# Date 1119432045 -7200
# Node ID 25a7459d4d4adfa13980c9fdd76e7fa397e6a3e1
# Parent  80ac7ac3733c75f202afbe0b2c6c9d4a21c39ce1
pointer equality for sml/nj

diff -r 80ac7ac3733c -r 25a7459d4d4a src/Pure/IsaMakefile
--- 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	\
diff -r 80ac7ac3733c -r 25a7459d4d4a src/Pure/ML-Systems/smlnj-ptreql.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;
diff -r 80ac7ac3733c -r 25a7459d4d4a src/Pure/ML-Systems/smlnj.ML
--- 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 *)