# HG changeset patch
# User wenzelm
# Date 1154000585 -7200
# Node ID 435601e8e53da3bfb13de0356286b19e171c9310
# Parent  6ea469c0331417ea799c9f8af21142a1c7d58e3d
removed obsolete equal_abs_elim(_list);

diff -r 6ea469c03314 -r 435601e8e53d src/Pure/drule.ML
--- a/src/Pure/drule.ML	Thu Jul 27 13:43:04 2006 +0200
+++ b/src/Pure/drule.ML	Thu Jul 27 13:43:05 2006 +0200
@@ -67,8 +67,6 @@
   val equals_cong: thm
   val imp_cong: thm
   val swap_prems_eq: thm
-  val equal_abs_elim: cterm  -> thm -> thm
-  val equal_abs_elim_list: cterm list -> thm -> thm
   val asm_rl: thm
   val cut_rl: thm
   val revcut_rl: thm
@@ -914,24 +912,6 @@
 end;
 
 
-(** Derived rules mainly for METAHYPS **)
-
-(*Given the term "a", takes (%x.t)==(%x.u) to t[a/x]==u[a/x]*)
-fun equal_abs_elim ca eqth =
-  let val {thy=thya, t=a, ...} = rep_cterm ca
-      and combth = combination eqth (reflexive ca)
-      val {thy,prop,...} = rep_thm eqth
-      val (abst,absu) = Logic.dest_equals prop
-      val cert = cterm_of (Theory.merge (thy,thya))
-  in  transitive (symmetric (beta_conversion false (cert (abst$a))))
-           (transitive combth (beta_conversion false (cert (absu$a))))
-  end
-  handle THM _ => raise THM("equal_abs_elim", 0, [eqth]);
-
-(*Calling equal_abs_elim with multiple terms*)
-fun equal_abs_elim_list cts th = foldr (uncurry equal_abs_elim) th (rev cts);
-
-
 (* global schematic variables *)
 
 fun unvarify th =