--- a/src/HOL/Tools/TFL/casesplit.ML Thu May 30 16:53:32 2013 +0200
+++ b/src/HOL/Tools/TFL/casesplit.ML Thu May 30 17:02:09 2013 +0200
@@ -13,13 +13,6 @@
structure CaseSplit: CASE_SPLIT =
struct
-(* beta-eta contract the theorem *)
-fun beta_eta_contract thm =
- let
- val thm2 = Thm.equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm
- val thm3 = Thm.equal_elim (Thm.eta_conversion (Thm.cprop_of thm2)) thm2
- in thm3 end;
-
(* make a casethm from an induction thm *)
val cases_thm_of_induct_thm =
Seq.hd o (ALLGOALS (fn i => REPEAT (etac Drule.thin_rl i)));
@@ -62,10 +55,10 @@
val cPv = ctermify (Envir.subst_term_types type_insts Pv);
val cDv = ctermify (Envir.subst_term_types type_insts Dv);
in
- (beta_eta_contract
+ Conv.fconv_rule Drule.beta_eta_conversion
(case_thm
|> Thm.instantiate (type_cinsts, [])
- |> Thm.instantiate ([], [(cPv, abs_ct), (cDv, free_ct)])))
+ |> Thm.instantiate ([], [(cPv, abs_ct), (cDv, free_ct)]))
end;