--- a/ROOT.ML	Wed Jan 30 03:46:22 2013 +0000
+++ b/ROOT.ML	Wed Jan 30 09:33:06 2013 +0000
@@ -14,8 +14,8 @@
 no_document 
 use_thys ["thys/turing_basic",
           "thys/turing_hoare", 
-	  "thys/uncomputable"(*, 
+	  "thys/uncomputable", 
 	  "thys/abacus", 
 	  "thys/rec_def", 
 	  "thys/recursive",
-          "thys/UF"*)]
+          "thys/UF"]