# HG changeset patch
# User nipkow
# Date 792921315 -3600
# Node ID 8e22076cd3caf7f2da1369db2b72f93f73820324
# Parent  516f9e349a16b87048aadf801d26109e59a80799
Improved test for looping rewrite rules.

diff -r 516f9e349a16 -r 8e22076cd3ca src/Pure/thm.ML
--- 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));