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