Hilbert_Classical: sequential loading due to @{prf}, which joins within a critical section (via options);

--- 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";