# HG changeset patch
# User nipkow
# Date 844090192 -7200
# Node ID fd26cd4da8cfee9a6d37c782e501d59329ac4861
# Parent  ae1030e667451639175a952a3dd5f883aeceaf94
Inserted check for rewrite rules which introduce extra Vars on the rhs.

diff -r ae1030e66745 -r fd26cd4da8cf src/Pure/thm.ML
--- a/src/Pure/thm.ML	Mon Sep 30 11:10:22 1996 +0200
+++ b/src/Pure/thm.ML	Mon Sep 30 15:29:52 1996 +0200
@@ -1421,9 +1421,11 @@
       val (elhs,erhs) = Logic.dest_equals econcl
       val perm = var_perm(elhs,erhs) andalso not(elhs aconv erhs)
                                      andalso not(is_Var(elhs))
-  in
-     if not perm andalso loops sign prems (elhs,erhs) then
-       (prtm_warning "ignoring looping rewrite rule" sign prop; None)
+  in if not(term_vars(erhs) subset
+            (term_vars(elhs) union flat(map term_vars prems)))
+     then (prtm_warning "extra Var(s) on rhs" sign prop; None) else
+     if not perm andalso loops sign prems (elhs,erhs)
+     then (prtm_warning "ignoring looping rewrite rule" sign prop; None)
      else Some{thm=thm,lhs=lhs,perm=perm}
   end;