diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Tools/TFL/casesplit.ML
--- 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 *)