--- a/ROOT.ML	Wed Jan 23 20:18:40 2013 +0100
+++ b/ROOT.ML	Thu Jan 24 00:20:26 2013 +0100
@@ -12,9 +12,10 @@
 *)
   
 no_document 
-use_thys ["thys/turing_basic"(*,
-          "thys/truing_hoare", 
+use_thys ["thys/turing_basic",
+          "thys/turing_hoare", 
 	  "thys/uncomputable", 
 	  "thys/abacus", 
 	  "thys/rec_def", 
-	  "thys/recursive"*)]
+	  "thys/recursive",
+          "thys/UF"]