src/Pure/drule.ML
changeset 8406 a217b0cd304d
parent 8365 affb2989d238
child 8496 7e4a466b18d5
     1.1 --- a/src/Pure/drule.ML	Fri Mar 10 01:16:19 2000 +0100
     1.2 +++ b/src/Pure/drule.ML	Fri Mar 10 14:57:06 2000 +0100
     1.3 @@ -560,12 +560,12 @@
     1.4      in  (sign', tye', maxi')  end;
     1.5  in
     1.6  fun cterm_instantiate ctpairs0 th =
     1.7 -  let val (sign,tye,_) = foldr add_types (ctpairs0, (#sign(rep_thm th),[],0))
     1.8 +  let val (sign,tye,_) = foldr add_types (ctpairs0, (#sign(rep_thm th), Vartab.empty, 0))
     1.9        val tsig = #tsig(Sign.rep_sg sign);
    1.10 -      fun instT(ct,cu) = let val inst = subst_TVars tye
    1.11 +      fun instT(ct,cu) = let val inst = subst_TVars_Vartab tye
    1.12                           in (cterm_fun inst ct, cterm_fun inst cu) end
    1.13        fun ctyp2 (ix,T) = (ix, ctyp_of sign T)
    1.14 -  in  instantiate (map ctyp2 tye, map instT ctpairs0) th  end
    1.15 +  in  instantiate (map ctyp2 (Vartab.dest tye), map instT ctpairs0) th  end
    1.16    handle TERM _ =>
    1.17             raise THM("cterm_instantiate: incompatible signatures",0,[th])
    1.18         | TYPE (msg, _, _) => raise THM(msg, 0, [th])