--- a/src/HOL/Tools/datatype_rep_proofs.ML Thu Apr 17 22:22:19 2008 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Thu Apr 17 22:22:21 2008 +0200
@@ -607,7 +607,7 @@
val dt_induct_prop = DatatypeProp.make_ind descr sorts;
val dt_induct = SkipProof.prove_global thy6 []
(Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
- (fn prems => EVERY
+ (fn {prems, ...} => EVERY
[rtac indrule_lemma' 1,
(indtac rep_induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
EVERY (map (fn (prem, r) => (EVERY