shutdown future scheduler after (failed) SAT_Examples, to workaround interference problem with follow-up theory loading;
authorwenzelm
Wed Jul 22 10:45:35 2009 +0200 (2009-07-22)
changeset 3210877094a0bbc3e
parent 32107 47d0da617fcc
child 32109 ff3677972e3f
shutdown future scheduler after (failed) SAT_Examples, to workaround interference problem with follow-up theory loading;
src/HOL/ex/ROOT.ML
     1.1 --- a/src/HOL/ex/ROOT.ML	Tue Jul 21 23:42:29 2009 +0200
     1.2 +++ b/src/HOL/ex/ROOT.ML	Wed Jul 22 10:45:35 2009 +0200
     1.3 @@ -83,6 +83,7 @@
     1.4  (* requires a proof-generating SAT solver (zChaff or MiniSAT) to be *)
     1.5  (* installed:                                                       *)
     1.6  try use_thy "SAT_Examples";
     1.7 +Future.shutdown ();
     1.8  
     1.9  (* requires zChaff (or some other reasonably fast SAT solver) to be *)
    1.10  (* installed:                                                       *)