# HG changeset patch
# User wenzelm
# Date 1185375947 -7200
# Node ID a15c13a54ab5fb017ea974a2ce4bc5216783f4d7
# Parent  6e8d5a05ffe844d79b8aa70e13c597a87ad11b1a
Secure.use_noncritical root;

diff -r 6e8d5a05ffe8 -r a15c13a54ab5 src/Pure/Isar/session.ML
--- a/src/Pure/Isar/session.ML	Wed Jul 25 17:05:45 2007 +0200
+++ b/src/Pure/Isar/session.ML	Wed Jul 25 17:05:47 2007 +0200
@@ -84,11 +84,13 @@
      (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 ()));
-      ThyInfo.time_use root;
+      Secure.use_noncritical root;
       finish ()))
     |> setmp_noncritical Proofterm.proofs level
     |> setmp_noncritical print_mode (modes @ ! print_mode)
-    |> setmp_noncritical Multithreading.max_threads max_threads) ()
+    |> setmp_noncritical Multithreading.max_threads
+      (if Multithreading.available then max_threads
+       else (if max_threads = 1 then () else warning "Multithreading support unavailable"; 1))) ()
   handle exn => (Output.error_msg (Toplevel.exn_message exn); exit 1);
 
 end;