# HG changeset patch
# User paulson
# Date 847796230 -3600
# Node ID acb0afbf61a306b243eb5c1a53711cdf25b34769
# Parent  8b365a3a6ed195ca100c9b2411bd1c7b28980230
Changed some mem calls to be monomorphic

diff -r 8b365a3a6ed1 -r acb0afbf61a3 src/Pure/unify.ML
--- a/src/Pure/unify.ML	Tue Nov 12 11:43:16 1996 +0100
+++ b/src/Pure/unify.ML	Tue Nov 12 11:57:10 1996 +0100
@@ -145,7 +145,7 @@
 	| occur (Bound _)  = false
 	| occur (Free _)  = false
 	| occur (Var (w,_))  = 
-	    if w mem !seen then false
+	    if mem_ix (w, !seen) then false
 	    else if v=w then true
 	      (*no need to lookup: v has no assignment*)
 	    else (seen := w:: !seen;  
@@ -208,7 +208,7 @@
 	| occur (Bound _)  = NoOcc
 	| occur (Free _)  = NoOcc
 	| occur (Var (w,_))  = 
-	    if w mem !seen then NoOcc
+	    if mem_ix (w, !seen) then NoOcc
 	    else if v=w then Rigid
 	    else (seen := w:: !seen;  
 	          case  Envir.lookup(env,w)  of