src/Pure/axclass.ML
changeset 33315 784c1b09d485
parent 33278 ba9f52f56356
child 33969 1e7ca47c6c3d
     1.1 --- a/src/Pure/axclass.ML	Thu Oct 29 16:15:33 2009 +0100
     1.2 +++ b/src/Pure/axclass.ML	Thu Oct 29 16:34:44 2009 +0100
     1.3 @@ -311,7 +311,7 @@
     1.4          (Binding.name (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 ((Binding.conceal (Binding.name c'), thm), [Thm.kind_internal])
     1.8 +      #> PureThy.add_thm ((Binding.conceal (Binding.name c'), thm), [])
     1.9        #> snd
    1.10        #> Sign.restore_naming thy
    1.11        #> pair (Const (c, T))))