Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/datatype_package.ML
changeset 18799 f137c5e971f5
parent 18751 38dc4ff2a32b
child 18857 c4b4fbd74ffb 
--- a/src/HOL/Tools/datatype_package.ML	Fri Jan 27 18:29:33 2006 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Fri Jan 27 19:03:02 2006 +0100
@@ -369,7 +369,7 @@
       [(("", proj index), [InductAttrib.induct_type name]),
        (("", exhaustion), [InductAttrib.cases_type name])];
     fun unnamed_rule i =
-      (("", proj i), [Drule.kind_internal, InductAttrib.induct_type ""]);
+      (("", proj i), [PureThy.kind_internal, InductAttrib.induct_type ""]);
   in
     PureThy.add_thms
       (List.concat (map named_rules infos) @
isabelle