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