Replaced datatype_info by datatype_info_err.
--- 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);