--- a/src/Pure/sign.ML Thu Nov 13 15:14:14 1997 +0100
+++ b/src/Pure/sign.ML Thu Nov 13 17:55:27 1997 +0100
@@ -75,6 +75,7 @@
val pprint_typ: sg -> typ -> pprint_args -> unit
val certify_typ: sg -> typ -> typ
val certify_term: sg -> term -> term * typ * int
+ val read_raw_typ: sg * (indexname -> sort option) -> string -> typ
val read_typ: sg * (indexname -> sort option) -> string -> typ
val infer_types: sg -> (indexname -> typ option) ->
(indexname -> sort option) -> string list -> bool
@@ -476,15 +477,17 @@
fun err_in_type s =
error ("The error(s) above occurred in type " ^ quote s);
-fun read_raw_typ syn tsig spaces def_sort str =
+fun rd_raw_typ syn tsig spaces def_sort str =
intrn_tycons spaces
(Syntax.read_typ syn (Type.get_sort tsig def_sort (intrn_sort spaces)) str
handle ERROR => err_in_type str);
-
+
+fun read_raw_typ (sg as Sg (_, {tsig, syn, spaces, ...}), def_sort) str =
+ (check_stale sg; rd_raw_typ syn tsig spaces def_sort str);
+
(*read and certify typ wrt a signature*)
-fun read_typ (sg as Sg (_, {tsig, syn, spaces, ...}), def_sort) str =
- (check_stale sg;
- Type.cert_typ tsig (read_raw_typ syn tsig spaces def_sort str)
+fun read_typ (sg, def_sort) str =
+ (Type.cert_typ (tsig_of sg) (read_raw_typ (sg, def_sort) str)
handle TYPE (msg, _, _) => (error_msg msg; err_in_type str));
@@ -659,7 +662,7 @@
(* add type abbreviations *)
fun read_abbr syn tsig spaces (t, vs, rhs_src) =
- (t, vs, read_raw_typ syn tsig spaces (K None) rhs_src)
+ (t, vs, rd_raw_typ syn tsig spaces (K None) rhs_src)
handle ERROR => error ("in type abbreviation " ^ t);
fun ext_abbrs rd_abbr (syn, tsig, ctab, (path, spaces), data) abbrs =
@@ -707,7 +710,7 @@
fun read_const syn tsig (path, spaces) (c, ty_src, mx) =
- (c, read_raw_typ syn tsig spaces (K None) ty_src, mx)
+ (c, rd_raw_typ syn tsig spaces (K None) ty_src, mx)
handle ERROR => err_in_const (const_name path c mx);
fun ext_cnsts rd_const syn_only prmode (syn, tsig, ctab, (path, spaces), data) raw_consts =