src/Pure/General/secure.ML
changeset 31330 7bfbd0e07a40
parent 30672 beaadd5af500
child 31473 fd341ca4b8de
--- a/src/Pure/General/secure.ML	Mon Jun 01 23:28:02 2009 +0200
+++ b/src/Pure/General/secure.ML	Mon Jun 01 23:28:04 2009 +0200
@@ -9,6 +9,7 @@
   val set_secure: unit -> unit
   val is_secure: unit -> bool
   val deny_secure: string -> unit
+  val secure_mltext: unit -> unit
   val use_text: use_context -> int * string -> bool -> string -> unit
   val use_file: use_context -> bool -> string -> unit
   val toplevel_pp: string list -> string -> unit