# HG changeset patch
# User nipkow
# Date 792239400 -3600
# Node ID 4f9c8503d1c58c3ade7be9528bebe430a3fc8888
# Parent  55d15c603e3a57992d734c653f1fed8c28f69167
Improved check for looping conditional rewrite rules.

diff -r 55d15c603e3a -r 4f9c8503d1c5 src/Pure/thm.ML
--- 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));