# HG changeset patch
# User wenzelm
# Date 1248252335 -7200
# Node ID 77094a0bbc3e3bb1b1737dca6de5840f5d989b5d
# Parent  47d0da617fccd6210332b2ee4d6d00693fe63bc8
shutdown future scheduler after (failed) SAT_Examples, to workaround interference problem with follow-up theory loading;

diff -r 47d0da617fcc -r 77094a0bbc3e src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Tue Jul 21 23:42:29 2009 +0200
+++ b/src/HOL/ex/ROOT.ML	Wed Jul 22 10:45:35 2009 +0200
@@ -83,6 +83,7 @@
 (* requires a proof-generating SAT solver (zChaff or MiniSAT) to be *)
 (* installed:                                                       *)
 try use_thy "SAT_Examples";
+Future.shutdown ();
 
 (* requires zChaff (or some other reasonably fast SAT solver) to be *)
 (* installed:                                                       *)