Updated read_insts to approximate simultaneous type checking of substitution
authornipkow
Tue Dec 14 14:02:52 1993 +0100 (1993-12-14)
changeset 1977c7179e687b2
parent 196 7646f5b4653c
child 198 0f0ff91b07f6
Updated read_insts to approximate simultaneous type checking of substitution
pairs.
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Mon Dec 13 18:50:03 1993 +0100
     1.2 +++ b/src/Pure/sign.ML	Tue Dec 14 14:02:52 1993 +0100
     1.3 @@ -341,10 +341,12 @@
     1.4                        Some T => typ_subst_TVars tye T
     1.5                      | None => absent ixn;
     1.6              val (ct,tye2) = read_def_cterm (sign,types,sorts) (st,T);
     1.7 -            val cv = cterm_of sign (Var(ixn,typ_subst_TVars tye2 T))
     1.8 -        in ((cv,ct)::cts,tye2 @ tye) end
     1.9 +        in ((ixn,T,ct)::cts,tye2 @ tye) end
    1.10      val (cterms,tye') = foldl add_cterm (([],tye), vs);
    1.11 -in (map (fn (ixn,T) => (ixn,ctyp_of sign T)) tye', cterms) end;
    1.12 +in (map (fn (ixn,T) => (ixn,ctyp_of sign T)) tye',
    1.13 +    map (fn (ixn,T,ct)=> (cterm_of sign (Var(ixn,typ_subst_TVars tye' T)), ct))
    1.14 +        cterms)
    1.15 +end;
    1.16  
    1.17  end;
    1.18