src/FOLP/hypsubst.ML

--- a/src/FOLP/hypsubst.ML	Wed May 05 09:24:42 2010 +0200
+++ b/src/FOLP/hypsubst.ML	Wed May 05 18:25:34 2010 +0200
@@ -33,7 +33,7 @@
 
 exception EQ_VAR;
 
-fun loose (i,t) = 0 mem add_loose_bnos(t,i,[]);
+fun loose (i, t) = member (op =) (add_loose_bnos (t, i, [])) 0;
 
 (*It's not safe to substitute for a constant; consider 0=1.
   It's not safe to substitute for x=t[x] since x is not eliminated.