src/Pure/Isar/session.ML

--- a/src/Pure/Isar/session.ML	Tue Jul 24 21:51:18 2007 +0200
+++ b/src/Pure/Isar/session.ML	Tue Jul 24 22:53:46 2007 +0200
@@ -10,7 +10,7 @@
   val name: unit -> string
   val welcome: unit -> string
   val use_dir: string -> bool -> string list -> bool -> bool -> string -> bool ->
-    string list -> string -> string -> bool * string -> string -> int -> bool -> unit
+    string list -> string -> string -> bool * string -> string -> int -> bool -> int -> unit
   val finish: unit -> unit
 end;
 
@@ -79,15 +79,16 @@
   | dumping (cp, path) = SOME (cp, Path.explode path);
 
 fun use_dir root build modes reset info doc doc_graph doc_versions
-    parent name dump rpath level verbose =
-  setmp_noncritical print_mode (modes @ ! print_mode)
-    (setmp_noncritical Proofterm.proofs level (fn () =>
-      (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;
-       finish ()))) ()
+    parent name dump rpath level verbose max_threads =
+  ((fn () =>
+     (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;
+      finish ()))
+    |> setmp_noncritical Proofterm.proofs level
+    |> setmp_noncritical print_mode (modes @ ! print_mode)
+    |> setmp_noncritical Multithreading.max_threads max_threads) ()
   handle exn => (Output.error_msg (Toplevel.exn_message exn); exit 1);
 
-
 end;