changeset 979 | a29142d703bc |
parent 959 | 35c2e5e114c4 |
child 1023 | f5f36bdc8003 |
--- a/src/Pure/thm.ML Tue Mar 28 13:13:17 1995 +0200 +++ b/src/Pure/thm.ML Thu Mar 30 08:54:17 1995 +0200 @@ -1067,7 +1067,7 @@ (*simple test for looping rewrite*) fun loops sign prems (lhs,rhs) = is_Var(lhs) orelse - (is_Free(lhs) andalso (lhs mem (foldr add_term_frees (rhs::prems,[])))) orelse + (is_Free(lhs) andalso (exists (apl(lhs, Logic.occs)) (rhs::prems))) orelse (null(prems) andalso Pattern.matches (#tsig(Sign.rep_sg sign)) (lhs,rhs));