src/Pure/drule.ML
changeset 14340 bc93ffa674cc
parent 14081 6c0f67e2f8d5
child 14387 e96d5c42c4b0
     1.1 --- a/src/Pure/drule.ML	Mon Jan 05 23:10:32 2004 +0100
     1.2 +++ b/src/Pure/drule.ML	Tue Jan 06 10:38:14 2004 +0100
     1.3 @@ -757,8 +757,9 @@
     1.4  in
     1.5  fun cterm_instantiate ctpairs0 th =
     1.6    let val (sign,tye,_) = foldr add_types (ctpairs0, (#sign(rep_thm th), Vartab.empty, 0))
     1.7 -      fun instT(ct,cu) = let val inst = subst_TVars_Vartab tye
     1.8 -                         in (cterm_fun inst ct, cterm_fun inst cu) end
     1.9 +      fun instT(ct,cu) = 
    1.10 +        let val inst = cterm_of sign o subst_TVars_Vartab tye o term_of
    1.11 +        in (inst ct, inst cu) end
    1.12        fun ctyp2 (ix,T) = (ix, ctyp_of sign T)
    1.13    in  instantiate (map ctyp2 (Vartab.dest tye), map instT ctpairs0) th  end
    1.14    handle TERM _ =>