diff -r 5641981ec67d -r 74bd7bfb484b Pearl-jv/ROOT.ML
--- a/Pearl-jv/ROOT.ML	Mon May 03 08:52:15 2010 +0100
+++ b/Pearl-jv/ROOT.ML	Tue May 04 05:36:43 2010 +0100
@@ -1,6 +1,7 @@
 no_document use_thys ["../Nominal-General/Nominal2_Base", 
                       "../Nominal-General/Nominal2_Atoms", 
                       "../Nominal-General/Nominal2_Eqvt",
+                      "../Nominal-General/Nominal2_Supp",
                       "../Nominal-General/Atoms", 
                       "LaTeXsugar"];