diff -r 97e1f9c2cc46 -r c1ce129e6f9c src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Thu May 17 21:51:32 2007 +0200
+++ b/src/HOL/ex/ROOT.ML	Thu May 17 22:33:41 2007 +0200
@@ -79,3 +79,5 @@
 
 HTML.with_charset "utf-8" (no_document time_use_thy) "Hebrew";
 HTML.with_charset "utf-8" (no_document time_use_thy) "Chinese";
+
+time_use_thy "Unification";