src/Pure/ML/ml_compiler0.ML

--- a/src/Pure/ML/ml_compiler0.ML	Fri Mar 18 17:51:57 2016 +0100
+++ b/src/Pure/ML/ml_compiler0.ML	Fri Mar 18 17:58:19 2016 +0100
@@ -47,8 +47,6 @@
 
 fun use_text ({name_space, here, print, error, ...}: context) {line, file, verbose, debug} text =
   let
-    val _ = Secure.deny_ml ();
-
     val current_line = Unsynchronized.ref line;
     val in_buffer = Unsynchronized.ref (String.explode (ml_input line file text));
     val out_buffer = Unsynchronized.ref ([]: string list);