# HG changeset patch
# User wenzelm
# Date 1253463307 -7200
# Node ID 20f1edc87b7d74f4513bfb00f303801b32cd8bac
# Parent  fef7022dc5ab3a08be437715a227b0fba426a6a6
Hilbert_Classical: more precise control of parallel_proofs;

diff -r fef7022dc5ab -r 20f1edc87b7d src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Sun Sep 20 17:23:23 2009 +0200
+++ b/src/HOL/ex/ROOT.ML	Sun Sep 20 18:15:07 2009 +0200
@@ -68,8 +68,7 @@
   "Landau"
 ];
 
-Future.shutdown ();
-(setmp_noncritical proofs 2 (setmp_noncritical Multithreading.max_threads 1 use_thy))
+(setmp_noncritical proofs 2 (setmp_noncritical Goal.parallel_proofs 0 use_thy))
   "Hilbert_Classical";
 
 use_thy "SVC_Oracle";