Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Simplification: used Logic.occs instead of mem add_term_frees
authornipkow
Thu, 30 Mar 1995 08:54:17 +0200
changeset 979 a29142d703bc
parent 978 f7011b47ac38
child 980 33e3054b2871
Simplification: used Logic.occs instead of mem add_term_frees
src/Pure/thm.ML file | annotate | diff | comparison | revisions 
--- 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));
isabelle