diff -r 2f47291b6ff9 -r 9ffee4eb1ae1 Nominal/ROOT.ML
--- a/Nominal/ROOT.ML	Sun Aug 29 12:17:25 2010 +0800
+++ b/Nominal/ROOT.ML	Sun Aug 29 13:36:03 2010 +0800
@@ -3,6 +3,7 @@
 no_document use_thys
    ["Ex/Classical",    
     "Ex/CoreHaskell",
+    "Ex/Ex1",
     "Ex/ExPS3",
     "Ex/ExPS7",
     "Ex/ExPS8",
@@ -12,6 +13,7 @@
     "Ex/LetPat",
     "Ex/LetRec",
     "Ex/LetRec2",
+    "Ex/LetFun",
     "Ex/Modules",
     "Ex/SingleLet",
     "Ex/TypeSchemes",