# HG changeset patch
# User wenzelm
# Date 1198012901 -3600
# Node ID 832073e402ae9d8934fe1c5d33da6b2575aa348d
# Parent  a61554b1e7a953a37ce465a3cdf221bb98d630dc
removed obsolete use_noncritical (plain use is already non-critical);

diff -r a61554b1e7a9 -r 832073e402ae src/Pure/General/secure.ML
--- 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();";
 
diff -r a61554b1e7a9 -r 832073e402ae src/Pure/Isar/session.ML
--- a/src/Pure/Isar/session.ML	Tue Dec 18 22:21:40 2007 +0100
+++ b/src/Pure/Isar/session.ML	Tue Dec 18 22:21:41 2007 +0100
@@ -84,7 +84,7 @@
      (init reset parent name;
       Present.init build info doc doc_graph doc_versions (path ()) name
         (dumping dump) (get_rpath rpath) verbose (map ThyInfo.theory (ThyInfo.names ()));
-      Secure.use_noncritical root;
+      use root;
       finish ()))
     |> setmp_noncritical Proofterm.proofs level
     |> setmp_noncritical print_mode (modes @ print_mode_value ())