diff -r df3a952c6a67 -r 8728f7990f6d Nominal/ROOT.ML
--- a/Nominal/ROOT.ML	Wed Jun 23 15:21:04 2010 +0100
+++ b/Nominal/ROOT.ML	Wed Jun 23 15:40:00 2010 +0100
@@ -1,5 +1,6 @@
 quick_and_dirty := true;
 
+(*
 no_document use_thys
    ["Ex/Lambda",
     "Ex/LF",
@@ -17,3 +18,4 @@
     "Ex/Test"(*,
     "Manual/Term4"*)
     ];
+*)
\ No newline at end of file