src/HOL/Tools/datatype_package.ML
changeset 18799 f137c5e971f5
parent 18751 38dc4ff2a32b
child 18857 c4b4fbd74ffb
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Fri Jan 27 18:29:33 2006 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Fri Jan 27 19:03:02 2006 +0100
     1.3 @@ -369,7 +369,7 @@
     1.4        [(("", proj index), [InductAttrib.induct_type name]),
     1.5         (("", exhaustion), [InductAttrib.cases_type name])];
     1.6      fun unnamed_rule i =
     1.7 -      (("", proj i), [Drule.kind_internal, InductAttrib.induct_type ""]);
     1.8 +      (("", proj i), [PureThy.kind_internal, InductAttrib.induct_type ""]);
     1.9    in
    1.10      PureThy.add_thms
    1.11        (List.concat (map named_rules infos) @