standardize towards Thm.eta_long_conversion, which just does eta_long conversion;
authorwenzelm
Sat May 30 23:58:06 2015 +0200 (2015-05-30)
changeset 60319127c2f00ca94
parent 60318 ab785001b51d
child 60320 e7c0ca878120
standardize towards Thm.eta_long_conversion, which just does eta_long conversion;
src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
src/Pure/drule.ML
     1.1 --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Sat May 30 23:30:54 2015 +0200
     1.2 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Sat May 30 23:58:06 2015 +0200
     1.3 @@ -1934,10 +1934,10 @@
     1.4        (rtac @{thm polarise} 1 THEN atac 1)
     1.5        ORELSE
     1.6          (REPEAT_DETERM (etac @{thm conjE} 1 THEN etac @{thm drop_first_hypothesis} 1)
     1.7 -         THEN PRIMITIVE (Conv.fconv_rule Drule.eta_long_conversion)
     1.8 +         THEN PRIMITIVE (Conv.fconv_rule Thm.eta_long_conversion)
     1.9           THEN (REPEAT_DETERM (ex_expander_tac ctxt 1))
    1.10           THEN (TRY ((CHANGED o rewrite_goal_tac ctxt @{thms simp_meta}) 1))
    1.11 -         THEN PRIMITIVE (Conv.fconv_rule Drule.eta_long_conversion)
    1.12 +         THEN PRIMITIVE (Conv.fconv_rule Thm.eta_long_conversion)
    1.13           THEN
    1.14             (HEADGOAL atac
    1.15             ORELSE
    1.16 @@ -2160,7 +2160,7 @@
    1.17      | "replace_andrewsEQ" => nonfull_extcnf_combined_tac [Assumption]
    1.18      | "split_preprocessing" =>
    1.19           (REPEAT (HEADGOAL (split_simp_tac ctxt)))
    1.20 -         THEN TRY (PRIMITIVE (Conv.fconv_rule Drule.eta_long_conversion))
    1.21 +         THEN TRY (PRIMITIVE (Conv.fconv_rule Thm.eta_long_conversion))
    1.22           THEN HEADGOAL atac
    1.23  
    1.24      (*FIXME some of these could eventually be handled specially*)
     2.1 --- a/src/Pure/drule.ML	Sat May 30 23:30:54 2015 +0200
     2.2 +++ b/src/Pure/drule.ML	Sat May 30 23:58:06 2015 +0200
     2.3 @@ -75,7 +75,6 @@
     2.4    val binop_cong_rule: cterm -> thm -> thm -> thm
     2.5    val fun_cong_rule: thm -> cterm -> thm
     2.6    val beta_eta_conversion: cterm -> thm
     2.7 -  val eta_long_conversion: cterm -> thm
     2.8    val eta_contraction_rule: thm -> thm
     2.9    val norm_hhf_eq: thm
    2.10    val norm_hhf_eqs: thm list
    2.11 @@ -435,11 +434,6 @@
    2.12    let val thm = Thm.beta_conversion true ct
    2.13    in Thm.transitive thm (Thm.eta_conversion (Thm.rhs_of thm)) end;
    2.14  
    2.15 -fun eta_long_conversion ct =
    2.16 -  Thm.transitive
    2.17 -    (beta_eta_conversion ct)
    2.18 -    (Thm.symmetric (beta_eta_conversion (cterm_fun (Envir.eta_long []) ct)));
    2.19 -
    2.20  (*Contract all eta-redexes in the theorem, lest they give rise to needless abstractions*)
    2.21  fun eta_contraction_rule th =
    2.22    Thm.equal_elim (Thm.eta_conversion (Thm.cprop_of th)) th;