Hilbert_Classical: disable multithreading altogether, otherwise proof normalization will fork futures independently of Goal.parallel_proofs;
1.1 --- a/src/HOL/ex/ROOT.ML Wed Jun 02 11:09:26 2010 +0200
1.2 +++ b/src/HOL/ex/ROOT.ML Wed Jun 02 13:18:21 2010 +0200
1.3 @@ -70,7 +70,7 @@
1.4 HTML.with_charset "utf-8" (no_document use_thys)
1.5 ["Hebrew", "Chinese", "Serbian"];
1.6
1.7 -(setmp_noncritical proofs 2 (setmp_noncritical Goal.parallel_proofs 0 use_thy))
1.8 +(setmp_noncritical proofs 2 (setmp_noncritical Multithreading.max_threads 1 use_thy))
1.9 "Hilbert_Classical";
1.10
1.11 use_thy "SVC_Oracle";