diff -r acfdd493f5c4 -r 5de27a5fc5ed src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Thu Apr 21 18:56:03 2005 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Thu Apr 21 18:57:18 2005 +0200
@@ -1362,10 +1362,10 @@
 	val tys_before = add_term_tfrees (prop_of th,[])
 	val th1 = varifyT th
 	val tys_after = add_term_tvars (prop_of th1,[])
-	val tyinst = map (fn (bef,(i,_)) =>
+	val tyinst = map (fn (bef, iS) =>
 			     (case try (Lib.assoc (TFree bef)) lambda of
-				  SOME ty => (i,ctyp_of sg ty)
-				| NONE => (i,ctyp_of sg (TFree bef))
+				  SOME ty => (ctyp_of sg (TVar iS), ctyp_of sg ty)
+				| NONE => (ctyp_of sg (TVar iS), ctyp_of sg (TFree bef))
 			     ))
 			 (zip tys_before tys_after)
 	val res = Drule.instantiate (tyinst,[]) th1