src/Pure/sign.ML
changeset 4227 a5c947d7c56c
parent 4140 c62df16811fe
child 4228 22e3f0368c85
     1.1 --- a/src/Pure/sign.ML	Thu Nov 13 15:14:14 1997 +0100
     1.2 +++ b/src/Pure/sign.ML	Thu Nov 13 17:55:27 1997 +0100
     1.3 @@ -75,6 +75,7 @@
     1.4    val pprint_typ: sg -> typ -> pprint_args -> unit
     1.5    val certify_typ: sg -> typ -> typ
     1.6    val certify_term: sg -> term -> term * typ * int
     1.7 +  val read_raw_typ: sg * (indexname -> sort option) -> string -> typ
     1.8    val read_typ: sg * (indexname -> sort option) -> string -> typ
     1.9    val infer_types: sg -> (indexname -> typ option) ->
    1.10      (indexname -> sort option) -> string list -> bool
    1.11 @@ -476,15 +477,17 @@
    1.12  fun err_in_type s =
    1.13    error ("The error(s) above occurred in type " ^ quote s);
    1.14  
    1.15 -fun read_raw_typ syn tsig spaces def_sort str =
    1.16 +fun rd_raw_typ syn tsig spaces def_sort str =
    1.17    intrn_tycons spaces
    1.18      (Syntax.read_typ syn (Type.get_sort tsig def_sort (intrn_sort spaces)) str
    1.19        handle ERROR => err_in_type str);
    1.20 -  
    1.21 +
    1.22 +fun read_raw_typ (sg as Sg (_, {tsig, syn, spaces, ...}), def_sort) str =
    1.23 +  (check_stale sg; rd_raw_typ syn tsig spaces def_sort str);
    1.24 +
    1.25  (*read and certify typ wrt a signature*)
    1.26 -fun read_typ (sg as Sg (_, {tsig, syn, spaces, ...}), def_sort) str =
    1.27 -  (check_stale sg;
    1.28 -    Type.cert_typ tsig (read_raw_typ syn tsig spaces def_sort str)
    1.29 +fun read_typ (sg, def_sort) str =
    1.30 +  (Type.cert_typ (tsig_of sg) (read_raw_typ (sg, def_sort) str)
    1.31        handle TYPE (msg, _, _) => (error_msg msg; err_in_type str));
    1.32  
    1.33  
    1.34 @@ -659,7 +662,7 @@
    1.35  (* add type abbreviations *)
    1.36  
    1.37  fun read_abbr syn tsig spaces (t, vs, rhs_src) =
    1.38 -  (t, vs, read_raw_typ syn tsig spaces (K None) rhs_src)
    1.39 +  (t, vs, rd_raw_typ syn tsig spaces (K None) rhs_src)
    1.40      handle ERROR => error ("in type abbreviation " ^ t);
    1.41  
    1.42  fun ext_abbrs rd_abbr (syn, tsig, ctab, (path, spaces), data) abbrs =
    1.43 @@ -707,7 +710,7 @@
    1.44  
    1.45  
    1.46  fun read_const syn tsig (path, spaces) (c, ty_src, mx) =
    1.47 -  (c, read_raw_typ syn tsig spaces (K None) ty_src, mx)
    1.48 +  (c, rd_raw_typ syn tsig spaces (K None) ty_src, mx)
    1.49      handle ERROR => err_in_const (const_name path c mx);
    1.50  
    1.51  fun ext_cnsts rd_const syn_only prmode (syn, tsig, ctab, (path, spaces), data) raw_consts =