diff -r d8903f0002e5 -r 5e2d381b0695 src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Tue Nov 10 13:05:35 2009 +0100
+++ b/src/HOL/ex/ROOT.ML	Tue Nov 10 13:17:50 2009 +0100
@@ -67,6 +67,9 @@
   "Landau"
 ];
 
+HTML.with_charset "utf-8" (no_document use_thys)
+  ["Hebrew", "Chinese", "Serbian"];
+
 (setmp_noncritical proofs 2 (setmp_noncritical Goal.parallel_proofs 0 use_thy))
   "Hilbert_Classical";
 
@@ -74,12 +77,10 @@
 if getenv "SVC_HOME" = "" then ()
 else use_thy "svc_test";
 
-(*requires a proof-generating SAT solver (zChaff or MiniSAT)*)
-try use_thy "SAT_Examples";
-
 (*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"];
+(*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) *)