--- a/src/Pure/drule.ML Sat May 30 23:30:54 2015 +0200
+++ b/src/Pure/drule.ML Sat May 30 23:58:06 2015 +0200
@@ -75,7 +75,6 @@
val binop_cong_rule: cterm -> thm -> thm -> thm
val fun_cong_rule: thm -> cterm -> thm
val beta_eta_conversion: cterm -> thm
- val eta_long_conversion: cterm -> thm
val eta_contraction_rule: thm -> thm
val norm_hhf_eq: thm
val norm_hhf_eqs: thm list
@@ -435,11 +434,6 @@
let val thm = Thm.beta_conversion true ct
in Thm.transitive thm (Thm.eta_conversion (Thm.rhs_of thm)) end;
-fun eta_long_conversion ct =
- Thm.transitive
- (beta_eta_conversion ct)
- (Thm.symmetric (beta_eta_conversion (cterm_fun (Envir.eta_long []) ct)));
-
(*Contract all eta-redexes in the theorem, lest they give rise to needless abstractions*)
fun eta_contraction_rule th =
Thm.equal_elim (Thm.eta_conversion (Thm.cprop_of th)) th;