src/HOL/Tools/TFL/casesplit.ML

 val atomize_goals = MetaSimplifier.rewrite_goals_rule Data.atomize;
 
 (* beta-eta contract the theorem *)
 fun beta_eta_contract thm =
     let
-      val thm2 = equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm
-      val thm3 = equal_elim (Thm.eta_conversion (Thm.cprop_of thm2)) thm2
+      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)));