src/HOL/ROOT

--- a/src/HOL/ROOT	Sat Feb 01 21:09:53 2014 +0100
+++ b/src/HOL/ROOT	Sat Feb 01 21:43:23 2014 +0100
@@ -572,8 +572,7 @@
     Sudoku
 (* FIXME
 (*requires a proof-generating SAT solver (zChaff or MiniSAT)*)
-(*global side-effects ahead!*)
-try use_thy "SAT_Examples";   (* FIXME try!? (not really a proper test) *)
+    SAT_Examples
 *)
   files "document/root.bib" "document/root.tex"