changeset 3915 | 0eb9b9dd4de6 |
parent 3893 | 5a1f22e7b359 |
child 3963 | 29c5ec9ecbaa |
--- a/src/Pure/logic.ML Fri Oct 17 11:09:34 1997 +0200 +++ b/src/Pure/logic.ML Fri Oct 17 11:10:13 1997 +0200 @@ -364,7 +364,7 @@ fun looptest sign prems lhs rhs = is_Var (head_of lhs) orelse - (exists (apl (lhs,occs)) (rhs :: prems)) + (exists (apl (lhs, op occs)) (rhs :: prems)) orelse (null prems andalso Pattern.matches (#tsig (Sign.rep_sg sign)) (lhs, rhs));