# HG changeset patch
# User wenzelm
# Date 1119372957 -7200
# Node ID 4699288139f4f92ee035297a097e3ecf0ddc1780
# Parent  0842635545c3212d323a73c6205176c3cf191e84
proper implementation of pointer_eq;

diff -r 0842635545c3 -r 4699288139f4 src/Pure/ML-Systems/mosml.ML
--- a/src/Pure/ML-Systems/mosml.ML	Tue Jun 21 18:55:44 2005 +0200
+++ b/src/Pure/ML-Systems/mosml.ML	Tue Jun 21 18:55:57 2005 +0200
@@ -19,12 +19,7 @@
 
 (** ML system related **)
 
-(*proper implementation available?*)
-fun pointer_eq (x:''a, y) = false;
-
-
-(* Poly/ML emulation *)
-
+load "Obj";
 load "Bool";
 load "Int";
 load "Real";
@@ -33,6 +28,10 @@
 load "Process";
 load "FileSys";
 
+(*low-level pointer equality*)
+local val cast : 'a -> int = Obj.magic
+in fun pointer_eq (x:'a, y:'a) = (cast x = cast y) end;
+
 (*proper implementation available?*)
 structure IntInf =
 struct
@@ -93,6 +92,7 @@
       f x;
 end;
 
+
 (* ML command execution *)
 
 (*Can one redirect 'use' directly to an instream?*)