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.
Improved test for looping rewrite rules.
authornipkow
Thu, 16 Feb 1995 08:55:15 +0100
changeset 900 8e22076cd3ca
parent 899 516f9e349a16
child 901 77795af99315
Improved test for looping rewrite rules.
src/Pure/thm.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/thm.ML	Wed Feb 15 20:02:47 1995 +0100
+++ b/src/Pure/thm.ML	Thu Feb 16 08:55:15 1995 +0100
@@ -1056,7 +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
+  (is_Free(lhs) andalso (lhs mem (foldr add_term_frees (rhs::prems,[])))) orelse
   (null(prems) andalso
    Pattern.matches (#tsig(Sign.rep_sg sign)) (lhs,rhs));
isabelle