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;