src/Pure/drule.ML
changeset 14340 bc93ffa674cc
parent 14081 6c0f67e2f8d5
child 14387 e96d5c42c4b0
equal deleted inserted replaced
14339:ec575b7bde7a 14340:bc93ffa674cc
   755           handle Type.TUNIFY => raise TYPE("Ill-typed instantiation", [T,U], [t,u])
   755           handle Type.TUNIFY => raise TYPE("Ill-typed instantiation", [T,U], [t,u])
   756     in  (sign', tye', maxi')  end;
   756     in  (sign', tye', maxi')  end;
   757 in
   757 in
   758 fun cterm_instantiate ctpairs0 th =
   758 fun cterm_instantiate ctpairs0 th =
   759   let val (sign,tye,_) = foldr add_types (ctpairs0, (#sign(rep_thm th), Vartab.empty, 0))
   759   let val (sign,tye,_) = foldr add_types (ctpairs0, (#sign(rep_thm th), Vartab.empty, 0))
   760       fun instT(ct,cu) = let val inst = subst_TVars_Vartab tye
   760       fun instT(ct,cu) = 
   761                          in (cterm_fun inst ct, cterm_fun inst cu) end
   761         let val inst = cterm_of sign o subst_TVars_Vartab tye o term_of
       
   762         in (inst ct, inst cu) end
   762       fun ctyp2 (ix,T) = (ix, ctyp_of sign T)
   763       fun ctyp2 (ix,T) = (ix, ctyp_of sign T)
   763   in  instantiate (map ctyp2 (Vartab.dest tye), map instT ctpairs0) th  end
   764   in  instantiate (map ctyp2 (Vartab.dest tye), map instT ctpairs0) th  end
   764   handle TERM _ =>
   765   handle TERM _ =>
   765            raise THM("cterm_instantiate: incompatible signatures",0,[th])
   766            raise THM("cterm_instantiate: incompatible signatures",0,[th])
   766        | TYPE (msg, _, _) => raise THM(msg, 0, [th])
   767        | TYPE (msg, _, _) => raise THM(msg, 0, [th])