diff -r df54b5365477 -r e4e64a0b0b6b src/HOL/Tools/induct_method.ML
--- a/src/HOL/Tools/induct_method.ML	Fri Jul 16 13:24:41 1999 +0200
+++ b/src/HOL/Tools/induct_method.ML	Fri Jul 16 13:25:45 1999 +0200
@@ -29,7 +29,7 @@
 
 (* induct_rule *)
 
-fun kind_rule Type = (#induction oo DatatypePackage.datatype_info, Sign.intern_tycon)
+fun kind_rule Type = (#induction oo DatatypePackage.datatype_info_err, Sign.intern_tycon)
   | kind_rule Set = ((#induct o #2) oo InductivePackage.get_inductive, Sign.intern_const)
   | kind_rule Function = (#induct oo RecdefPackage.get_recdef, Sign.intern_const);