src/HOL/Tools/datatype_package.ML
changeset 10279 b223a9a3350e
parent 10214 77349ed89f45
child 10525 3e21ab3e5114
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Thu Oct 19 21:23:15 2000 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Thu Oct 19 21:23:47 2000 +0200
     1.3 @@ -298,8 +298,8 @@
     1.4            |> RuleCases.name (RuleCases.get thm);
     1.5  
     1.6      fun add (ths, (name, {index, descr, induction, exhaustion, ...}: datatype_info)) =
     1.7 -      (("", proj index (length descr) induction), [InductMethod.induct_type_global name]) ::
     1.8 -      (("", exhaustion), [InductMethod.cases_type_global name]) :: ths;
     1.9 +      (("", proj index (length descr) induction), [InductAttrib.induct_type_global name]) ::
    1.10 +      (("", exhaustion), [InductAttrib.cases_type_global name]) :: ths;
    1.11    in #1 o PureThy.add_thms (foldl add ([], infos)) end;
    1.12  
    1.13