Fixed bug in rewriter (fun impc) discovered by Marcus Moore.
authornipkow
Mon Nov 22 09:20:28 1993 +0100 (1993-11-22)
changeset 134595fda4879b6
parent 133 2322fd6d57a1
child 135 493308514ea8
Fixed bug in rewriter (fun impc) discovered by Marcus Moore.
src/Pure/thm.ML
     1.1 --- a/src/Pure/thm.ML	Fri Nov 19 12:54:16 1993 +0100
     1.2 +++ b/src/Pure/thm.ML	Mon Nov 22 09:20:28 1993 +0100
     1.3 @@ -986,7 +986,8 @@
     1.4              val unit = seq (trace_thm "Adding rewrite rule:") rthms
     1.5              val mss' = add_simps(mss,rthms)
     1.6              val ((sg2,hyps2),u') = botc mss' (sghy1,u)
     1.7 -        in ((sg2,hyps2\s'), Logic.mk_implies(s',u')) end
     1.8 +            val hyps2' = if s' mem hyps1 then hyps2 else hyps2\s'
     1.9 +        in ((sg2,hyps2'), Logic.mk_implies(s',u')) end
    1.10  
    1.11    in botc end;
    1.12