--- 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 =