src/Pure/axclass.ML
changeset 35845 e5980f0ad025
parent 35669 a91c7ed801b8
child 35854 d452abc96459
     1.1 --- a/src/Pure/axclass.ML	Sat Mar 20 02:23:41 2010 +0100
     1.2 +++ b/src/Pure/axclass.ML	Sat Mar 20 17:33:11 2010 +0100
     1.3 @@ -309,7 +309,7 @@
     1.4      |-> (fn const' as Const (c'', _) =>
     1.5        Thm.add_def false true
     1.6          (Binding.name (Thm.def_name c'), Logic.mk_equals (Const (c, T'), const'))
     1.7 -      #>> Thm.varifyT
     1.8 +      #>> Thm.varifyT_global
     1.9        #-> (fn thm => add_inst_param (c, tyco) (c'', thm)
    1.10        #> PureThy.add_thm ((Binding.conceal (Binding.name c'), thm), [])
    1.11        #> snd