--- a/src/HOL/Nominal/nominal_package.ML Thu Jul 05 19:59:01 2007 +0200
+++ b/src/HOL/Nominal/nominal_package.ML Thu Jul 05 20:01:26 2007 +0200
@@ -1083,7 +1083,7 @@
(Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
(fn prems => EVERY
[rtac indrule_lemma' 1,
- (DatatypeAux.indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
+ (DatatypeAux.indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
EVERY (map (fn (prem, r) => (EVERY
[REPEAT (eresolve_tac Abs_inverse_thms' 1),
simp_tac (HOL_basic_ss addsimps [symmetric r]) 1,