# HG changeset patch
# User nipkow
# Date 751892023 -3600
# Node ID c378e56d4a4b461078742af79935c5c4b265e730
# Parent  3406bd994306a2610475e0eed9eb040066f59c42
added function del_simps

diff -r 3406bd994306 -r c378e56d4a4b src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Oct 28 17:40:50 1993 +0100
+++ b/src/Pure/thm.ML	Fri Oct 29 11:53:43 1993 +0100
@@ -29,6 +29,7 @@
   val biresolution: bool -> (bool*thm)list -> int -> thm -> thm Sequence.seq   
   val combination: thm -> thm -> thm   
   val concl_of: thm -> term   
+  val del_simps: meta_simpset * thm list -> meta_simpset
   val dest_state: thm * int -> (term*term)list * term list * term * term
   val empty_mss: meta_simpset
   val eq_assumption: int -> thm -> thm   
@@ -811,21 +812,37 @@
      else Some{thm=thm,lhs=lhs}
   end;
 
+local
+ fun eq({thm=Thm{prop=p1,...},...}:rrule,
+        {thm=Thm{prop=p2,...},...}:rrule) = p1 aconv p2
+in
+
 fun add_simp(mss as Mss{net,congs,primes,prems,mk_rews},
              thm as Thm{sign,prop,...}) =
-  let fun eq({thm=Thm{prop=p1,...},...}:rrule,
-             {thm=Thm{prop=p2,...},...}:rrule) = p1 aconv p2
-  in case mk_rrule thm of
-       None => mss
-     | Some(rrule as {lhs,...}) =>
-         Mss{net= (Net.insert_term((lhs,rrule),net,eq)
-                   handle Net.INSERT =>
-                   (prtm "Warning: ignoring duplicate rewrite rule" sign prop;
-                    net)),
+  case mk_rrule thm of
+    None => mss
+  | Some(rrule as {lhs,...}) =>
+      Mss{net= (Net.insert_term((lhs,rrule),net,eq)
+                handle Net.INSERT =>
+                  (prtm "Warning: ignoring duplicate rewrite rule" sign prop;
+                   net)),
+          congs=congs, primes=primes, prems=prems,mk_rews=mk_rews};
+
+fun del_simp(mss as Mss{net,congs,primes,prems,mk_rews},
+             thm as Thm{sign,prop,...}) =
+  case mk_rrule thm of
+    None => mss
+  | Some(rrule as {lhs,...}) =>
+      Mss{net= (Net.delete_term((lhs,rrule),net,eq)
+                handle Net.INSERT =>
+                 (prtm "Warning: rewrite rule not in simpset" sign prop;
+                  net)),
              congs=congs, primes=primes, prems=prems,mk_rews=mk_rews}
-  end;
+
+end;
 
 val add_simps = foldl add_simp;
+val del_simps = foldl del_simp;
 
 fun mss_of thms = add_simps(empty_mss,thms);