# HG changeset patch
# User wenzelm
# Date 1248797855 -7200
# Node ID 8721c74c53826df089b4241d33361de419e874ae
# Parent  d302f1c9e356fd4aabe1cb908c2e3d485d4945b6
Hilbert_Classical: sequential loading due to @{prf}, which joins within a critical section (via options);

diff -r d302f1c9e356 -r 8721c74c5382 src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Tue Jul 28 16:30:23 2009 +0200
+++ b/src/HOL/ex/ROOT.ML	Tue Jul 28 18:17:35 2009 +0200
@@ -68,7 +68,8 @@
   "Landau"
 ];
 
-setmp_noncritical proofs 2 use_thy "Hilbert_Classical";
+(setmp_noncritical proofs 2 (setmp_noncritical Multithreading.max_threads 1 use_thy))
+  "Hilbert_Classical";
 
 
 use_thy "SVC_Oracle";