--- a/Nominal/ROOT.ML	Fri Dec 16 16:01:12 2011 +0900
+++ b/Nominal/ROOT.ML	Sat Dec 17 20:03:37 2011 +0000
@@ -32,8 +32,6 @@
 quick_and_dirty := true;
 
 no_document use_thys
-   ["Ex/Classical",    
-    "Ex/Let"
-   ];
+   ["Ex/Let"];