src/Pure/sign.ML
changeset 1414 036e072b215a
parent 1393 73b6b003c6ca
child 1458 fd510875fb71
     1.1 --- a/src/Pure/sign.ML	Fri Dec 22 10:26:57 1995 +0100
     1.2 +++ b/src/Pure/sign.ML	Fri Dec 22 10:30:06 1995 +0100
     1.3 @@ -405,7 +405,10 @@
     1.4  
     1.5  fun ext_cnsts rd_const syn_only (syn, tsig, ctab) raw_consts =
     1.6    let
     1.7 -    fun prep_const (c, ty, mx) = (c, varifyT (cert_typ tsig (no_tvars ty)), mx)
     1.8 +    fun prep_const (c, ty, mx) = 
     1.9 +	  (c, 
    1.10 +	   compress_type (varifyT (cert_typ tsig (no_tvars ty))), 
    1.11 +	   mx)
    1.12        handle TYPE (msg, _, _) => (writeln msg; err_in_const (Syntax.const_name c mx));
    1.13  
    1.14      val consts = map (prep_const o rd_const syn tsig) raw_consts;