src/Pure/drule.ML
changeset 10403 2955ee2424ce
parent 9862 96138f29545e
child 10414 f7aeff3e9e1e
     1.1 --- a/src/Pure/drule.ML	Mon Nov 06 22:49:16 2000 +0100
     1.2 +++ b/src/Pure/drule.ML	Mon Nov 06 22:50:01 2000 +0100
     1.3 @@ -178,7 +178,7 @@
     1.4    error("Instantiation of " ^ Syntax.string_of_vname ixn ^ " fails");
     1.5  
     1.6  fun read_insts sign (rtypes,rsorts) (types,sorts) used insts =
     1.7 -let val {tsig,...} = Sign.rep_sg sign
     1.8 +let
     1.9      fun split([],tvs,vs) = (tvs,vs)
    1.10        | split((sv,st)::l,tvs,vs) = (case Symbol.explode sv of
    1.11                    "'"::cs => split(l,(Syntax.indexname cs,st)::tvs,vs)
    1.12 @@ -188,7 +188,7 @@
    1.13          let val ixn = ("'" ^ a,i);
    1.14              val S = case rsorts ixn of Some S => S | None => absent ixn;
    1.15              val T = Sign.read_typ (sign,sorts) st;
    1.16 -        in if Type.typ_instance(tsig,T,TVar(ixn,S)) then (ixn,T)
    1.17 +        in if Sign.typ_instance sign (T, TVar(ixn,S)) then (ixn,T)
    1.18             else inst_failure ixn
    1.19          end
    1.20      val tye = map readT tvs;
    1.21 @@ -654,12 +654,11 @@
    1.22          val maxi = Int.max(maxidx, Int.max(maxt, maxu));
    1.23          val sign' = Sign.merge(sign, Sign.merge(signt, signu))
    1.24          val (tye',maxi') = Type.unify (#tsig(Sign.rep_sg sign')) maxi tye (T,U)
    1.25 -          handle Type.TUNIFY => raise TYPE("add_types", [T,U], [t,u])
    1.26 +          handle Type.TUNIFY => raise TYPE("Ill-typed instantiation", [T,U], [t,u])
    1.27      in  (sign', tye', maxi')  end;
    1.28  in
    1.29  fun cterm_instantiate ctpairs0 th =
    1.30    let val (sign,tye,_) = foldr add_types (ctpairs0, (#sign(rep_thm th), Vartab.empty, 0))
    1.31 -      val tsig = #tsig(Sign.rep_sg sign);
    1.32        fun instT(ct,cu) = let val inst = subst_TVars_Vartab tye
    1.33                           in (cterm_fun inst ct, cterm_fun inst cu) end
    1.34        fun ctyp2 (ix,T) = (ix, ctyp_of sign T)