diff -r c0eac04ae3b4 -r c34347ec7ab3 Nominal/ROOT.ML
--- a/Nominal/ROOT.ML	Sat Apr 03 22:31:11 2010 +0200
+++ b/Nominal/ROOT.ML	Sun Apr 04 21:39:28 2010 +0200
@@ -1,11 +1,7 @@
 quick_and_dirty := true;
 
 no_document use_thys
-   ["Nominal2_Base",
-    "Nominal2_Eqvt",
-    "Nominal2_Atoms",
-    "Nominal2_Supp",
-    "Ex/ExLam",
+   ["Ex/ExLam",
     "Ex/ExLF",
     "Ex/Ex1",
     "Ex/Ex1rec",