1.1 --- a/src/Pure/thm.ML	Thu Oct 28 17:40:50 1993 +0100
     1.2 +++ b/src/Pure/thm.ML	Fri Oct 29 11:53:43 1993 +0100
     1.3 @@ -29,6 +29,7 @@
     1.4    val biresolution: bool -> (bool*thm)list -> int -> thm -> thm Sequence.seq   
     1.5    val combination: thm -> thm -> thm   
     1.6    val concl_of: thm -> term   
     1.7 +  val del_simps: meta_simpset * thm list -> meta_simpset
     1.8    val dest_state: thm * int -> (term*term)list * term list * term * term
     1.9    val empty_mss: meta_simpset
    1.10    val eq_assumption: int -> thm -> thm   
    1.11 @@ -811,21 +812,37 @@
    1.12       else Some{thm=thm,lhs=lhs}
    1.13    end;
    1.14  
    1.15 +local
    1.16 + fun eq({thm=Thm{prop=p1,...},...}:rrule,
    1.17 +        {thm=Thm{prop=p2,...},...}:rrule) = p1 aconv p2
    1.18 +in
    1.19 +
    1.20  fun add_simp(mss as Mss{net,congs,primes,prems,mk_rews},
    1.21               thm as Thm{sign,prop,...}) =
    1.22 -  let fun eq({thm=Thm{prop=p1,...},...}:rrule,
    1.23 -             {thm=Thm{prop=p2,...},...}:rrule) = p1 aconv p2
    1.24 -  in case mk_rrule thm of
    1.25 -       None => mss
    1.26 -     | Some(rrule as {lhs,...}) =>
    1.27 -         Mss{net= (Net.insert_term((lhs,rrule),net,eq)
    1.28 -                   handle Net.INSERT =>
    1.29 -                   (prtm "Warning: ignoring duplicate rewrite rule" sign prop;
    1.30 -                    net)),
    1.31 +  case mk_rrule thm of
    1.32 +    None => mss
    1.33 +  | Some(rrule as {lhs,...}) =>
    1.34 +      Mss{net= (Net.insert_term((lhs,rrule),net,eq)
    1.35 +                handle Net.INSERT =>
    1.36 +                  (prtm "Warning: ignoring duplicate rewrite rule" sign prop;
    1.37 +                   net)),
    1.38 +          congs=congs, primes=primes, prems=prems,mk_rews=mk_rews};
    1.39 +
    1.40 +fun del_simp(mss as Mss{net,congs,primes,prems,mk_rews},
    1.41 +             thm as Thm{sign,prop,...}) =
    1.42 +  case mk_rrule thm of
    1.43 +    None => mss
    1.44 +  | Some(rrule as {lhs,...}) =>
    1.45 +      Mss{net= (Net.delete_term((lhs,rrule),net,eq)
    1.46 +                handle Net.INSERT =>
    1.47 +                 (prtm "Warning: rewrite rule not in simpset" sign prop;
    1.48 +                  net)),
    1.49               congs=congs, primes=primes, prems=prems,mk_rews=mk_rews}
    1.50 -  end;
    1.51 +
    1.52 +end;
    1.53  
    1.54  val add_simps = foldl add_simp;
    1.55 +val del_simps = foldl del_simp;
    1.56  
    1.57  fun mss_of thms = add_simps(empty_mss,thms);
    1.58