doc-src/LaTeXsugar/Sugar/ROOT.ML

--- a/doc-src/LaTeXsugar/Sugar/ROOT.ML	Wed Dec 29 13:51:17 2010 +0100
+++ b/doc-src/LaTeXsugar/Sugar/ROOT.ML	Wed Dec 29 17:34:41 2010 +0100
@@ -1,4 +1,6 @@
-no_document use_thy "LaTeXsugar";
-no_document use_thy "OptionalSugar";
+no_document use_thys [
+  "~~/src/HOL/Library/LaTeXsugar",
+  "~~/src/HOL/Library/OptionalSugar"
+];
 use_thy "Sugar";