# HG changeset patch
# User oheimb
# Date 856019073 -3600
# Node ID 373daa468a740e4644509ae45ceae5b384c9c8aa
# Parent  69c1b8a493de6c5c6bda2de1796dbb847b5419ac
added del_congs

diff -r 69c1b8a493de -r 373daa468a74 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Feb 14 16:01:43 1997 +0100
+++ b/src/Pure/thm.ML	Sat Feb 15 16:04:33 1997 +0100
@@ -144,6 +144,7 @@
   val del_simps         : meta_simpset * thm list -> meta_simpset
   val mss_of            : thm list -> meta_simpset
   val add_congs         : meta_simpset * thm list -> meta_simpset
+  val del_congs         : meta_simpset * thm list -> meta_simpset
   val add_simprocs	: meta_simpset *
     (Sign.sg * term * (Sign.sg -> term -> thm option) * stamp) list -> meta_simpset
   val del_simprocs	: meta_simpset *
@@ -1526,7 +1527,7 @@
 val del_simps = foldl del_simp;
 
 
-(* congs *)
+(* add_congs *)
 
 fun add_cong (Mss {rules, congs, procs, bounds, prems, mk_rews, termless}, thm) =
   let
@@ -1543,6 +1544,23 @@
 val (op add_congs) = foldl add_cong;
 
 
+(* del_congs *)
+
+fun del_cong (Mss {rules, congs, procs, bounds, prems, mk_rews, termless}, thm) =
+  let
+    val (lhs, _) = Logic.dest_equals (concl_of thm) handle TERM _ =>
+      raise SIMPLIFIER ("Congruence not a meta-equality", thm);
+(*   val lhs = Pattern.eta_contract lhs; *)
+    val (a, _) = dest_Const (head_of lhs) handle TERM _ =>
+      raise SIMPLIFIER ("Congruence must start with a constant", thm);
+  in
+    mk_mss (rules, filter (fn (x,_)=> x<>a) congs, procs, bounds,
+      prems, mk_rews, termless)
+  end;
+
+val (op del_congs) = foldl del_cong;
+
+
 (* add_simprocs *)
 
 fun add_simproc (mss as Mss {rules, congs, procs, bounds, prems, mk_rews, termless},