shutdown future scheduler after (failed) SAT_Examples, to workaround interference problem with follow-up theory loading;

--- 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:                                                       *)