diff -r 41137dc935ff -r 8193bbaa07fe Pearl/ROOT.ML --- a/Pearl/ROOT.ML Sun Nov 14 12:09:14 2010 +0000 +++ b/Pearl/ROOT.ML Sun Nov 14 16:34:47 2010 +0000 @@ -1,6 +1,6 @@ -no_document use_thys ["../Nominal-General/Nominal2_Base", - "../Nominal-General/Nominal2_Eqvt", - "../Nominal-General/Atoms", +no_document use_thys ["../Nominal/Nominal2_Base", + "../Nominal/Nominal2_Eqvt", + "../Nominal/Atoms", "LaTeXsugar"]; use_thys ["Paper"]; \ No newline at end of file