src/Pure/thm.ML

               else let val thm = Thm{sign=sg1,hyps=[s'],prop=s',maxidx= ~1}
                    in (mk_rews thm, add_prems(mss,[thm])) end
             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;
 
 
 (*** Meta-rewriting: rewrites t to u and returns the theorem t==u ***)