# HG changeset patch
# User wenzelm
# Date 1251472035 -7200
# Node ID 700ed1f4c576f4ef5bac9968287e73046b8e4835
# Parent  0a94e1f264ce6b2d8a20a52bedfbe87d2d000456
SAT_Examples: removed obsolete Future.shutdown() workaround -- internal exception propagation should now work reliably;
misc tuning and cleanup;

diff -r 0a94e1f264ce -r 700ed1f4c576 src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Fri Aug 28 11:31:49 2009 +0200
+++ b/src/HOL/ex/ROOT.ML	Fri Aug 28 17:07:15 2009 +0200
@@ -72,25 +72,16 @@
 (setmp_noncritical proofs 2 (setmp_noncritical Multithreading.max_threads 1 use_thy))
   "Hilbert_Classical";
 
-
 use_thy "SVC_Oracle";
-
-fun svc_enabled () = getenv "SVC_HOME" <> "";
-fun if_svc_enabled f x = if svc_enabled () then f x else ();
-
-if_svc_enabled use_thy "svc_test";
-
+if getenv "SVC_HOME" = "" then ()
+else use_thy "svc_test";
 
-(* requires a proof-generating SAT solver (zChaff or MiniSAT) to be *)
-(* installed:                                                       *)
+(*requires a proof-generating SAT solver (zChaff or MiniSAT)*)
 try use_thy "SAT_Examples";
-Future.shutdown ();
 
-(* requires zChaff (or some other reasonably fast SAT solver) to be *)
-(* installed:                                                       *)
-if getenv "ZCHAFF_HOME" <> "" then
-  use_thy "Sudoku"
-else ();
+(*requires zChaff (or some other reasonably fast SAT solver)*)
+if getenv "ZCHAFF_HOME" = "" then ()
+else use_thy "Sudoku";
 
 HTML.with_charset "utf-8" (no_document use_thys)
   ["Hebrew", "Chinese", "Serbian"];