--- a/src/Pure/General/secure.ML Fri Oct 31 15:15:10 2014 +0100
+++ b/src/Pure/General/secure.ML Fri Oct 31 16:03:45 2014 +0100
@@ -13,7 +13,6 @@
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
- val commit: unit -> unit
end;
structure Secure: SECURE =
@@ -32,8 +31,6 @@
(** critical operations **)
-(* ML evaluation *)
-
fun secure_mltext () = deny_secure "Cannot evaluate ML source in secure mode";
val raw_use_text = use_text;
@@ -45,12 +42,5 @@
fun toplevel_pp path pp = (secure_mltext (); raw_toplevel_pp ML_Parse.global_context path pp);
-
-(* global evaluation *)
-
-val use_global = raw_use_text ML_Parse.global_context (0, "") false;
-
-fun commit () = use_global "commit();"; (*commit is dynamically bound!*)
-
end;