# HG changeset patch
# User wenzelm
# Date 895683396 -7200
# Node ID 8637b29e6c38737f33bbb5c91d7eeeb0277dc4e5
# Parent  226f2cde9f4d1bfab27301ea349ca124de3a5ed0
added is_stale;

diff -r 226f2cde9f4d -r 8637b29e6c38 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Wed May 20 18:56:00 1998 +0200
+++ b/src/Pure/sign.ML	Wed May 20 18:56:36 1998 +0200
@@ -37,6 +37,7 @@
   val eq_sg: sg * sg -> bool
   val same_sg: sg * sg -> bool
   val is_draft: sg -> bool
+  val is_stale: sg -> bool
   val const_type: sg -> string -> typ option
   val classes: sg -> class list
   val defaultS: sg -> sort
@@ -193,6 +194,8 @@
       else raise TERM ("Stale signature: " ^ str_of_sg sg, [])
   | check_stale _ = sys_error "Sign.check_stale";
 
+fun is_stale sg = (check_stale sg; false) handle TERM _ => true;
+
 fun self_ref (sg as Sg (_, {self, ...})) = (check_stale sg; self);
 
 fun deref (SgRef (Some (ref sg))) = sg