export deny_secure;

--- a/src/Pure/General/secure.ML	Sat Feb 16 16:43:56 2008 +0100
+++ b/src/Pure/General/secure.ML	Sat Feb 16 16:43:57 2008 +0100
@@ -9,6 +9,7 @@
 sig
   val set_secure: unit -> unit
   val is_secure: unit -> bool
+  val deny_secure: string -> unit
   val use_text: string -> (string -> unit) * (string -> 'a) -> bool -> string -> unit
   val use_file: (string -> unit) * (string -> 'a) -> bool -> string -> unit
   val use: string -> unit