--- 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