diff -r 6aa98a113e6c -r a5da7b6aff8f Pearl/ROOT.ML
--- a/Pearl/ROOT.ML	Wed Mar 16 21:07:50 2011 +0100
+++ b/Pearl/ROOT.ML	Wed Mar 16 21:14:43 2011 +0100
@@ -1,5 +1,5 @@
 no_document use_thys ["../Nominal/Nominal2_Base", 
                       "../Nominal/Atoms", 
-                      "LaTeXsugar"];
+                      "~~/src/HOL/Library/LaTeXsugar"];
 
 use_thys ["Paper"];
\ No newline at end of file