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