# HG changeset patch
# User nipkow
# Date 755874172 -3600
# Node ID 7c7179e687b21d2ba21a56d4eec6a96032cd0f34
# Parent  7646f5b4653c8cb7b8c03e9fc1c169a0a32420b9
Updated read_insts to approximate simultaneous type checking of substitution
pairs.

diff -r 7646f5b4653c -r 7c7179e687b2 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Mon Dec 13 18:50:03 1993 +0100
+++ b/src/Pure/sign.ML	Tue Dec 14 14:02:52 1993 +0100
@@ -341,10 +341,12 @@
                       Some T => typ_subst_TVars tye T
                     | None => absent ixn;
             val (ct,tye2) = read_def_cterm (sign,types,sorts) (st,T);
-            val cv = cterm_of sign (Var(ixn,typ_subst_TVars tye2 T))
-        in ((cv,ct)::cts,tye2 @ tye) end
+        in ((ixn,T,ct)::cts,tye2 @ tye) end
     val (cterms,tye') = foldl add_cterm (([],tye), vs);
-in (map (fn (ixn,T) => (ixn,ctyp_of sign T)) tye', cterms) end;
+in (map (fn (ixn,T) => (ixn,ctyp_of sign T)) tye',
+    map (fn (ixn,T,ct)=> (cterm_of sign (Var(ixn,typ_subst_TVars tye' T)), ct))
+        cterms)
+end;
 
 end;