# HG changeset patch
# User nipkow
# Date 753956428 -3600
# Node ID 595fda4879b6e381bef9bbc66c59be1d9ebbde28
# Parent  2322fd6d57a1413a093c2b245b96365f5c4ba92c
Fixed bug in rewriter (fun impc) discovered by Marcus Moore.

diff -r 2322fd6d57a1 -r 595fda4879b6 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Nov 19 12:54:16 1993 +0100
+++ b/src/Pure/thm.ML	Mon Nov 22 09:20:28 1993 +0100
@@ -986,7 +986,8 @@
             val unit = seq (trace_thm "Adding rewrite rule:") rthms
             val mss' = add_simps(mss,rthms)
             val ((sg2,hyps2),u') = botc mss' (sghy1,u)
-        in ((sg2,hyps2\s'), Logic.mk_implies(s',u')) end
+            val hyps2' = if s' mem hyps1 then hyps2 else hyps2\s'
+        in ((sg2,hyps2'), Logic.mk_implies(s',u')) end
 
   in botc end;