1.1 --- a/src/HOL/Import/proof_kernel.ML	Sat Mar 20 02:23:41 2010 +0100
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Sat Mar 20 17:33:11 2010 +0100
     1.3 @@ -1418,7 +1418,7 @@
     1.4          val _ = message "INST_TYPE:"
     1.5          val _ = if_debug pth hth
     1.6          val tys_before = OldTerm.add_term_tfrees (prop_of th,[])
     1.7 -        val th1 = Thm.varifyT th
     1.8 +        val th1 = Thm.varifyT_global th
     1.9          val tys_after = OldTerm.add_term_tvars (prop_of th1,[])
    1.10          val tyinst = map (fn (bef, iS) =>
    1.11                               (case try (Lib.assoc (TFree bef)) lambda of
    1.12 @@ -2028,7 +2028,7 @@
    1.13                                   names'
    1.14                                   (thy1,th)
    1.15              val _ = ImportRecorder.add_specification names' th
    1.16 -            val res' = Thm.unvarify res
    1.17 +            val res' = Thm.unvarify_global res
    1.18              val hth = HOLThm(rens,res')
    1.19              val rew = rewrite_hol4_term (concl_of res') thy'
    1.20              val th  = equal_elim rew res'