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