diff -r cc6e281d8f72 -r 0a36825b16c1 Nominal/ROOT.ML
--- a/Nominal/ROOT.ML	Fri Aug 27 02:08:36 2010 +0800
+++ b/Nominal/ROOT.ML	Fri Aug 27 03:37:17 2010 +0800
@@ -1,21 +1,19 @@
-quick_and_dirty := true;
 
-(*
+
 no_document use_thys
-   ["Ex/Lambda",
-    "Ex/LF",
-    "Ex/SingleLet",
-    "Ex/Ex1rec",
-    "Ex/Ex2",
-    "Ex/Ex3",
-    "Ex/ExLet",
-    "Ex/ExLetRec",
-    "Ex/TypeSchemes",
-    "Ex/Modules",
+   ["Ex/Classical",    
+    "Ex/CoreHaskell",
     "Ex/ExPS3",
     "Ex/ExPS7",
-    "Ex/CoreHaskell",
-    "Ex/Test"(*,
-    "Manual/Term4"*)
+    "Ex/ExPS8",
+    "Ex/LF",
+    "Ex/Lambda",
+    "Ex/Let",
+    "Ex/LetPat",
+    "Ex/LetRec",
+    "Ex/LetRec2",
+    "Ex/Modules",
+    "Ex/SingleLet",
+    "Ex/TypeSchemes",
+    "Ex/TypeVarsTest"
     ];
-*)
\ No newline at end of file