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/Pure/axclass.ML
changeset 27865 27a8ad9612a3
parent 27691 ce171cbd4b93
child 28014 fe36718702aa 
--- a/src/Pure/axclass.ML	Thu Aug 14 11:55:05 2008 +0200
+++ b/src/Pure/axclass.ML	Thu Aug 14 16:52:46 2008 +0200
@@ -374,7 +374,7 @@
           (Thm.def_name c', Logic.mk_equals (Const (c, T'), const'))
     #>> Thm.varifyT
     #-> (fn thm => add_inst_param (c, tyco) (c'', thm)
-    #> PureThy.add_thm ((c', thm), [PureThy.kind_internal])
+    #> PureThy.add_thm ((c', thm), [Thm.kind_internal])
     #> snd
     #> Sign.restore_naming thy
     #> pair (Const (c, T))))
isabelle