src/Pure/sign.ML
changeset 3969 9c742951a923
parent 3967 edd5ff9371f8
child 3975 ddeb5a0fd08d
     1.1 --- a/src/Pure/sign.ML	Tue Oct 21 18:15:43 1997 +0200
     1.2 +++ b/src/Pure/sign.ML	Wed Oct 22 11:36:29 1997 +0200
     1.3 @@ -508,9 +508,10 @@
     1.4        handle ERROR => err_in_type str);
     1.5    
     1.6  (*read and certify typ wrt a signature*)
     1.7 -fun read_typ (Sg {tsig, syn, spaces, ...}, def_sort) str =
     1.8 -  Type.cert_typ tsig (read_raw_typ syn tsig spaces def_sort str)
     1.9 -    handle TYPE (msg, _, _) => (error_msg msg; err_in_type str);
    1.10 +fun read_typ (sg as Sg {tsig, syn, spaces, ...}, def_sort) str =
    1.11 +  (check_stale sg;
    1.12 +    Type.cert_typ tsig (read_raw_typ syn tsig spaces def_sort str)
    1.13 +      handle TYPE (msg, _, _) => (error_msg msg; err_in_type str));
    1.14  
    1.15  
    1.16  
    1.17 @@ -565,6 +566,8 @@
    1.18  
    1.19  fun certify_term (sg as Sg {tsig, ...}) tm =
    1.20    let
    1.21 +    val _ = check_stale sg;
    1.22 +
    1.23      fun valid_const a T =
    1.24        (case const_type sg a of
    1.25          Some U => Type.typ_instance (tsig, T, U)