--- a/Quotient-Paper/ROOT.ML	Wed Mar 16 21:07:50 2011 +0100
+++ b/Quotient-Paper/ROOT.ML	Wed Mar 16 21:14:43 2011 +0100
@@ -1,5 +1,5 @@
 quick_and_dirty := true;
 no_document use_thys ["Quotient", 
-                      "LaTeXsugar",
-                      "$ISABELLE_HOME/src/HOL/Quotient_Examples/FSet" ];
+                      "~~/src/HOL/Library/LaTeXsugar",
+                      "~~/src/HOL/Quotient_Examples/FSet" ];
 use_thys ["Paper"];