--- a/src/HOL/Tools/datatype_abs_proofs.ML Thu Jul 05 19:59:01 2007 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML Thu Jul 05 20:01:26 2007 +0200
@@ -215,7 +215,7 @@
val induct' = cterm_instantiate ((map cert induct_Ps) ~~
(map cert insts)) induct;
val (tac, _) = Library.foldl mk_unique_tac
- (((rtac induct' THEN_ALL_NEW ObjectLogic.atomize_tac) 1
+ (((rtac induct' THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1
THEN rewtac (mk_meta_eq choice_eq), rec_intrs),
descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts);