export secure_mltext;
authorwenzelm
Mon, 01 Jun 2009 23:28:04 +0200
changeset 31330 7bfbd0e07a40
parent 31329 c8821a6297f9
child 31331 e44f1e4fa1f4
export secure_mltext;
src/Pure/General/secure.ML
--- 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