author | nipkow |
Wed, 08 Feb 1995 11:30:00 +0100 (1995-02-08) | |
changeset 898 | 4f9c8503d1c5 |
parent 897 | 55d15c603e3a |
child 899 | 516f9e349a16 |
src/Pure/thm.ML | file | annotate | diff | comparison | revisions |
--- a/src/Pure/thm.ML Tue Feb 07 17:36:48 1995 +0100 +++ b/src/Pure/thm.ML Wed Feb 08 11:30:00 1995 +0100 @@ -1056,6 +1056,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 (prems,[])))) orelse (null(prems) andalso Pattern.matches (#tsig(Sign.rep_sg sign)) (lhs,rhs));