# 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;