--- a/src/HOL/Tools/datatype_package.ML Thu Oct 19 21:23:15 2000 +0200
+++ b/src/HOL/Tools/datatype_package.ML Thu Oct 19 21:23:47 2000 +0200
@@ -298,8 +298,8 @@
|> RuleCases.name (RuleCases.get thm);
fun add (ths, (name, {index, descr, induction, exhaustion, ...}: datatype_info)) =
- (("", proj index (length descr) induction), [InductMethod.induct_type_global name]) ::
- (("", exhaustion), [InductMethod.cases_type_global name]) :: ths;
+ (("", proj index (length descr) induction), [InductAttrib.induct_type_global name]) ::
+ (("", exhaustion), [InductAttrib.cases_type_global name]) :: ths;
in #1 o PureThy.add_thms (foldl add ([], infos)) end;