# HG changeset patch
# User wenzelm
# Date 1433023086 -7200
# Node ID 127c2f00ca94877d7f6bfce3da79256ba5a94a94
# Parent  ab785001b51d4cde4c7e045cabd4d4b708d5e745
standardize towards Thm.eta_long_conversion, which just does eta_long conversion;

diff -r ab785001b51d -r 127c2f00ca94 src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Sat May 30 23:30:54 2015 +0200
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Sat May 30 23:58:06 2015 +0200
@@ -1934,10 +1934,10 @@
       (rtac @{thm polarise} 1 THEN atac 1)
       ORELSE
         (REPEAT_DETERM (etac @{thm conjE} 1 THEN etac @{thm drop_first_hypothesis} 1)
-         THEN PRIMITIVE (Conv.fconv_rule Drule.eta_long_conversion)
+         THEN PRIMITIVE (Conv.fconv_rule Thm.eta_long_conversion)
          THEN (REPEAT_DETERM (ex_expander_tac ctxt 1))
          THEN (TRY ((CHANGED o rewrite_goal_tac ctxt @{thms simp_meta}) 1))
-         THEN PRIMITIVE (Conv.fconv_rule Drule.eta_long_conversion)
+         THEN PRIMITIVE (Conv.fconv_rule Thm.eta_long_conversion)
          THEN
            (HEADGOAL atac
            ORELSE
@@ -2160,7 +2160,7 @@
     | "replace_andrewsEQ" => nonfull_extcnf_combined_tac [Assumption]
     | "split_preprocessing" =>
          (REPEAT (HEADGOAL (split_simp_tac ctxt)))
-         THEN TRY (PRIMITIVE (Conv.fconv_rule Drule.eta_long_conversion))
+         THEN TRY (PRIMITIVE (Conv.fconv_rule Thm.eta_long_conversion))
          THEN HEADGOAL atac
 
     (*FIXME some of these could eventually be handled specially*)
diff -r ab785001b51d -r 127c2f00ca94 src/Pure/drule.ML
--- 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;