diff -r 0255394a05da -r a217b0cd304d src/Pure/drule.ML
--- a/src/Pure/drule.ML	Fri Mar 10 01:16:19 2000 +0100
+++ b/src/Pure/drule.ML	Fri Mar 10 14:57:06 2000 +0100
@@ -560,12 +560,12 @@
     in  (sign', tye', maxi')  end;
 in
 fun cterm_instantiate ctpairs0 th =
-  let val (sign,tye,_) = foldr add_types (ctpairs0, (#sign(rep_thm th),[],0))
+  let val (sign,tye,_) = foldr add_types (ctpairs0, (#sign(rep_thm th), Vartab.empty, 0))
       val tsig = #tsig(Sign.rep_sg sign);
-      fun instT(ct,cu) = let val inst = subst_TVars tye
+      fun instT(ct,cu) = let val inst = subst_TVars_Vartab tye
                          in (cterm_fun inst ct, cterm_fun inst cu) end
       fun ctyp2 (ix,T) = (ix, ctyp_of sign T)
-  in  instantiate (map ctyp2 tye, map instT ctpairs0) th  end
+  in  instantiate (map ctyp2 (Vartab.dest tye), map instT ctpairs0) th  end
   handle TERM _ =>
            raise THM("cterm_instantiate: incompatible signatures",0,[th])
        | TYPE (msg, _, _) => raise THM(msg, 0, [th])