diff -r 551c5a8b6b2c -r 26d594a9b89f Quotient-Paper/ROOT.ML
--- a/Quotient-Paper/ROOT.ML	Thu Oct 28 14:03:46 2010 +0900
+++ b/Quotient-Paper/ROOT.ML	Thu Oct 28 14:12:30 2010 +0900
@@ -1,6 +1,5 @@
 quick_and_dirty := true;
 no_document use_thys ["Quotient", 
                       "LaTeXsugar",
-                      "../Nominal/FSet" ];
-
-use_thys ["Paper"];
\ No newline at end of file
+                      "$ISABELLE_HOME/src/HOL/Quotient_Examples/FSet" ];
+use_thys ["Paper"];