1.1 --- a/src/HOL/Import/proof_kernel.ML	Thu Jun 09 22:25:25 2011 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Thu Jun 09 23:12:02 2011 +0200
     1.3 @@ -1419,7 +1419,7 @@
     1.4                                  | NONE => (ctyp_of thy (TVar iS), ctyp_of thy (TFree bef))
     1.5                               ))
     1.6                           (zip tys_before tys_after)
     1.7 -        val res = Drule.instantiate (tyinst,[]) th1
     1.8 +        val res = Drule.instantiate_normalize (tyinst,[]) th1
     1.9          val hth = HOLThm([],res)
    1.10          val res = norm_hthm thy hth
    1.11          val _ = message "RESULT:"