# HG changeset patch
# User wenzelm
# Date 1275477501 -7200
# Node ID 0fb011773adcc55a3588b7cb7e124016ead619a9
# Parent  72c7e636067b85ed67dbbe0c3fa22a8fce5fdd7e
Hilbert_Classical: disable multithreading altogether, otherwise proof normalization will fork futures independently of Goal.parallel_proofs;

diff -r 72c7e636067b -r 0fb011773adc src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Wed Jun 02 11:09:26 2010 +0200
+++ b/src/HOL/ex/ROOT.ML	Wed Jun 02 13:18:21 2010 +0200
@@ -70,7 +70,7 @@
 HTML.with_charset "utf-8" (no_document use_thys)
   ["Hebrew", "Chinese", "Serbian"];
 
-(setmp_noncritical proofs 2 (setmp_noncritical Goal.parallel_proofs 0 use_thy))
+(setmp_noncritical proofs 2 (setmp_noncritical Multithreading.max_threads 1 use_thy))
   "Hilbert_Classical";
 
 use_thy "SVC_Oracle";