workaround bug in Type.expand_typ;
authorwenzelm
Thu Jun 09 11:02:14 1994 +0200 (1994-06-09)
changeset 418ab09293bccc7
parent 417 6bb9eb9cb02f
child 419 7c7e71be40c8
workaround bug in Type.expand_typ;
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Thu Jun 09 11:00:37 1994 +0200
     1.2 +++ b/src/Pure/sign.ML	Thu Jun 09 11:02:14 1994 +0200
     1.3 @@ -362,9 +362,15 @@
     1.4    (c, read_raw_typ syn tsig (K None) ty_src, mx)
     1.5      handle ERROR => err_in_const (const_name c mx);
     1.6  
     1.7 +(* FIXME move *)
     1.8 +fun no_tvars ty =
     1.9 +  if null (typ_tvars ty) then ty
    1.10 +  else raise_type "Illegal schematic type variable(s)" [ty] [];
    1.11 +
    1.12  fun ext_cnsts rd_const syn_only (syn, tsig, ctab) raw_consts =
    1.13    let
    1.14 -    fun prep_const (c, ty, mx) = (c, cert_typ tsig (varify_typ ty), mx)
    1.15 +    (* FIXME clean *)
    1.16 +    fun prep_const (c, ty, mx) = (c, varify_typ (cert_typ tsig (no_tvars ty)), mx)
    1.17        handle TYPE (msg, _, _) => (writeln msg; err_in_const (const_name c mx));
    1.18  
    1.19      val consts = map (prep_const o rd_const syn tsig) raw_consts;