--- a/src/Pure/General/secure.ML Tue Dec 18 22:21:40 2007 +0100
+++ b/src/Pure/General/secure.ML Tue Dec 18 22:21:41 2007 +0100
@@ -11,7 +11,6 @@
val is_secure: unit -> bool
val use_text: string -> (string -> unit) * (string -> 'a) -> bool -> string -> unit
val use_file: (string -> unit) * (string -> 'a) -> bool -> string -> unit
- val use_noncritical: string -> unit
val use: string -> unit
val commit: unit -> unit
val execute: string -> string
@@ -48,9 +47,6 @@
fun use name = use_file Output.ml_output true name;
-fun use_noncritical name = (* FIXME obsolete *)
- (secure_mltext (); orig_use_file Output.ml_output true name);
-
(*commit is dynamically bound!*)
fun commit () = orig_use_text "" Output.ml_output false "commit();";