# HG changeset patch
# User wenzelm
# Date 1243891684 -7200
# Node ID 7bfbd0e07a40b1778af631d91d584827010afcae
# Parent  c8821a6297f9804cb0fe6db3d50a01b97bcdf3ca
export secure_mltext;

diff -r c8821a6297f9 -r 7bfbd0e07a40 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