src/Pure/drule.ML
changeset 14643 130076a81b84
parent 14394 51b24127eef2
child 14824 336ade035a34
     1.1 --- a/src/Pure/drule.ML	Thu Apr 22 10:49:30 2004 +0200
     1.2 +++ b/src/Pure/drule.ML	Thu Apr 22 10:52:32 2004 +0200
     1.3 @@ -748,7 +748,7 @@
     1.4  
     1.5  (*Instantiate theorem th, reading instantiations under theory of th*)
     1.6  fun read_instantiate sinsts th =
     1.7 -    read_instantiate_sg (#sign (rep_thm th)) sinsts th;
     1.8 +    read_instantiate_sg (Thm.sign_of_thm th) sinsts th;
     1.9  
    1.10  
    1.11  (*Left-to-right replacements: tpairs = [...,(vi,ti),...].
    1.12 @@ -759,12 +759,12 @@
    1.13          and {sign=signu, t=u, T= U, maxidx=maxu,...} = rep_cterm cu;
    1.14          val maxi = Int.max(maxidx, Int.max(maxt, maxu));
    1.15          val sign' = Sign.merge(sign, Sign.merge(signt, signu))
    1.16 -        val (tye',maxi') = Type.unify (#tsig(Sign.rep_sg sign')) (tye, maxi) (T, U)
    1.17 +        val (tye',maxi') = Type.unify (Sign.tsig_of sign') (tye, maxi) (T, U)
    1.18            handle Type.TUNIFY => raise TYPE("Ill-typed instantiation", [T,U], [t,u])
    1.19      in  (sign', tye', maxi')  end;
    1.20  in
    1.21  fun cterm_instantiate ctpairs0 th =
    1.22 -  let val (sign,tye,_) = foldr add_types (ctpairs0, (#sign(rep_thm th), Vartab.empty, 0))
    1.23 +  let val (sign,tye,_) = foldr add_types (ctpairs0, (Thm.sign_of_thm th, Vartab.empty, 0))
    1.24        fun instT(ct,cu) = 
    1.25          let val inst = cterm_of sign o subst_TVars_Vartab tye o term_of
    1.26          in (inst ct, inst cu) end