src/FOLP/hypsubst.ML
changeset 36692 54b64d4ad524
parent 35762 af3ff2ba4c54
child 37744 3daaf23b9ab4
     1.1 --- a/src/FOLP/hypsubst.ML	Wed May 05 09:24:42 2010 +0200
     1.2 +++ b/src/FOLP/hypsubst.ML	Wed May 05 18:25:34 2010 +0200
     1.3 @@ -33,7 +33,7 @@
     1.4  
     1.5  exception EQ_VAR;
     1.6  
     1.7 -fun loose (i,t) = 0 mem add_loose_bnos(t,i,[]);
     1.8 +fun loose (i, t) = member (op =) (add_loose_bnos (t, i, [])) 0;
     1.9  
    1.10  (*It's not safe to substitute for a constant; consider 0=1.
    1.11    It's not safe to substitute for x=t[x] since x is not eliminated.