src/Pure/axclass.ML
changeset 27865 27a8ad9612a3
parent 27691 ce171cbd4b93
child 28014 fe36718702aa
     1.1 --- a/src/Pure/axclass.ML	Thu Aug 14 11:55:05 2008 +0200
     1.2 +++ b/src/Pure/axclass.ML	Thu Aug 14 16:52:46 2008 +0200
     1.3 @@ -374,7 +374,7 @@
     1.4            (Thm.def_name c', Logic.mk_equals (Const (c, T'), const'))
     1.5      #>> Thm.varifyT
     1.6      #-> (fn thm => add_inst_param (c, tyco) (c'', thm)
     1.7 -    #> PureThy.add_thm ((c', thm), [PureThy.kind_internal])
     1.8 +    #> PureThy.add_thm ((c', thm), [Thm.kind_internal])
     1.9      #> snd
    1.10      #> Sign.restore_naming thy
    1.11      #> pair (Const (c, T))))