diff -r 99d170aebb6e -r c1bb6480534f src/HOL/Tools/datatype_aux.ML
--- a/src/HOL/Tools/datatype_aux.ML	Fri Oct 28 22:27:44 2005 +0200
+++ b/src/HOL/Tools/datatype_aux.ML	Fri Oct 28 22:27:46 2005 +0200
@@ -111,7 +111,7 @@
   (List.nth (prems_of st, i - 1)) of
     _ $ (_ $ (f $ x) $ (g $ y)) =>
       let
-        val cong' = lift_rule (st, i) cong;
+        val cong' = Thm.lift_rule (Thm.cgoal_of st i) cong;
         val _ $ (_ $ (f' $ x') $ (g' $ y')) =
           Logic.strip_assums_concl (prop_of cong');
         val insts = map (pairself (cterm_of (#sign (rep_thm st))) o
@@ -151,7 +151,7 @@
     val prem = List.nth (prems_of state, i - 1);
     val params = Logic.strip_params prem;
     val (_, Type (tname, _)) = hd (rev params);
-    val exhaustion = lift_rule (state, i) (exh_thm_of tname);
+    val exhaustion = Thm.lift_rule (Thm.cgoal_of state i) (exh_thm_of tname);
     val prem' = hd (prems_of exhaustion);
     val _ $ (_ $ lhs $ _) = hd (rev (Logic.strip_assums_hyp prem'));
     val exhaustion' = cterm_instantiate [(cterm_of sg (head_of lhs),