src/HOL/Tools/TFL/casesplit.ML
changeset 52243 92bafa4235fa
parent 49340 25fc6e0da459
child 55236 8d61b0aa7a0d
     1.1 --- a/src/HOL/Tools/TFL/casesplit.ML	Thu May 30 16:53:32 2013 +0200
     1.2 +++ b/src/HOL/Tools/TFL/casesplit.ML	Thu May 30 17:02:09 2013 +0200
     1.3 @@ -13,13 +13,6 @@
     1.4  structure CaseSplit: CASE_SPLIT =
     1.5  struct
     1.6  
     1.7 -(* beta-eta contract the theorem *)
     1.8 -fun beta_eta_contract thm =
     1.9 -    let
    1.10 -      val thm2 = Thm.equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm
    1.11 -      val thm3 = Thm.equal_elim (Thm.eta_conversion (Thm.cprop_of thm2)) thm2
    1.12 -    in thm3 end;
    1.13 -
    1.14  (* make a casethm from an induction thm *)
    1.15  val cases_thm_of_induct_thm =
    1.16       Seq.hd o (ALLGOALS (fn i => REPEAT (etac Drule.thin_rl i)));
    1.17 @@ -62,10 +55,10 @@
    1.18        val cPv = ctermify (Envir.subst_term_types type_insts Pv);
    1.19        val cDv = ctermify (Envir.subst_term_types type_insts Dv);
    1.20      in
    1.21 -      (beta_eta_contract
    1.22 +      Conv.fconv_rule Drule.beta_eta_conversion
    1.23           (case_thm
    1.24              |> Thm.instantiate (type_cinsts, [])
    1.25 -            |> Thm.instantiate ([], [(cPv, abs_ct), (cDv, free_ct)])))
    1.26 +            |> Thm.instantiate ([], [(cPv, abs_ct), (cDv, free_ct)]))
    1.27      end;
    1.28  
    1.29