diff -r c8ff97d9f8da -r 7edbd5657702 ROOT.ML
--- a/ROOT.ML	Sun Jan 20 16:01:16 2013 +0000
+++ b/ROOT.ML	Tue Jan 22 14:38:56 2013 +0000
@@ -12,10 +12,9 @@
 *)
   
 no_document 
-use_thys ["turing_basic", 
-	  "uncomputable", 
-	  "abacus", 
-	  "rec_def", 
-	  "recursive", 
-	  "UF", 
-          "UTM"]
+use_thys ["thys/turing_basic"(*,
+          "thys/truing_hoare", 
+	  "thys/uncomputable", 
+	  "thys/abacus", 
+	  "thys/rec_def", 
+	  "thys/recursive"*)]