src/HOL/ex/ROOT.ML

--- a/src/HOL/ex/ROOT.ML	Fri Jan 13 17:39:41 2006 +0100
+++ b/src/HOL/ex/ROOT.ML	Sat Jan 14 17:14:06 2006 +0100
@@ -45,7 +45,7 @@
 if_svc_enabled time_use_thy "svc_test";
 
 (* requires zChaff with proof generation to be installed: *)
-time_use_thy "SAT_Examples" handle ERROR => ();
+try time_use_thy "SAT_Examples";
 
 (* requires zChaff (or some other reasonably fast SAT solver) to be installed: *)
 if getenv "ZCHAFF_HOME" <> "" then