# HG changeset patch
# User wenzelm
# Date 1203176637 -3600
# Node ID d920e4c8ba82f310f1f769571dac5bd1cdb49caf
# Parent  a58cc0cf41768ffbc734ac17db429d582ad3a6f7
export deny_secure;

diff -r a58cc0cf4176 -r d920e4c8ba82 src/Pure/General/secure.ML
--- 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