author | nipkow |
Mon, 22 Nov 1993 09:20:28 +0100 | |
changeset 134 | 595fda4879b6 |
parent 133 | 2322fd6d57a1 |
child 135 | 493308514ea8 |
src/Pure/thm.ML | file | annotate | diff | comparison | revisions |
--- 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;