# HG changeset patch
# User wenzelm
# Date 877512989 -7200
# Node ID 9c742951a923f2a333dbefa094e7fa4a131d5d52
# Parent  ec138de716d9ca7df5d958b5a82668d124dd8ab9
certify: check_stale;

diff -r ec138de716d9 -r 9c742951a923 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Tue Oct 21 18:15:43 1997 +0200
+++ b/src/Pure/sign.ML	Wed Oct 22 11:36:29 1997 +0200
@@ -508,9 +508,10 @@
       handle ERROR => err_in_type str);
   
 (*read and certify typ wrt a signature*)
-fun read_typ (Sg {tsig, syn, spaces, ...}, def_sort) str =
-  Type.cert_typ tsig (read_raw_typ syn tsig spaces def_sort str)
-    handle TYPE (msg, _, _) => (error_msg msg; err_in_type str);
+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)
+      handle TYPE (msg, _, _) => (error_msg msg; err_in_type str));
 
 
 
@@ -565,6 +566,8 @@
 
 fun certify_term (sg as Sg {tsig, ...}) tm =
   let
+    val _ = check_stale sg;
+
     fun valid_const a T =
       (case const_type sg a of
         Some U => Type.typ_instance (tsig, T, U)