changeset 36692 | 54b64d4ad524 |
parent 35762 | af3ff2ba4c54 |
child 37744 | 3daaf23b9ab4 |
--- 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.