changeset 33278 | ba9f52f56356 |
parent 33173 | b8ca12f6681a |
child 33315 | 784c1b09d485 |
--- a/src/Pure/axclass.ML Wed Oct 28 16:25:26 2009 +0100 +++ b/src/Pure/axclass.ML Wed Oct 28 16:25:27 2009 +0100 @@ -311,7 +311,7 @@ (Binding.name (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 ((Binding.name c', thm), [Thm.kind_internal]) + #> PureThy.add_thm ((Binding.conceal (Binding.name c'), thm), [Thm.kind_internal]) #> snd #> Sign.restore_naming thy #> pair (Const (c, T))))