--- a/src/HOL/Tools/TFL/casesplit.ML Sat May 15 21:41:32 2010 +0200
+++ b/src/HOL/Tools/TFL/casesplit.ML Sat May 15 21:50:05 2010 +0200
@@ -79,8 +79,8 @@
(* 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 *)