# HG changeset patch
# User wenzelm
# Date 1369926129 -7200
# Node ID 92bafa4235fa15e527a2ce7b01937c3fd8dd8fa7
# Parent  2d634bfa1bbf9c9184c8869ddd4ae5bb2ddc1463
prefer existing beta_eta_conversion;

diff -r 2d634bfa1bbf -r 92bafa4235fa src/HOL/Tools/TFL/casesplit.ML
--- 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;