diff -r 67063c5365e1 -r 8a3e63163910 Paper/ROOT.ML
--- a/Paper/ROOT.ML	Sun Feb 10 19:49:07 2013 +0000
+++ b/Paper/ROOT.ML	Sun Feb 10 20:56:08 2013 +0000
@@ -1,9 +1,9 @@
 no_document 
-use_thys ["../thys/turing_basic", 
-          "../thys/turing_hoare",
-          "../thys/uncomputable", 
-          "../thys/abacus"(*,
-          "../thys/rec_def",
-          "../thys/recursive"*)];
+use_thys ["../thys/Turing", 
+          "../thys/Turing_Hoare",
+          "../thys/Uncomputable", 
+          "../thys/Abacus",
+          "../thys/Rec_Def",
+          "../thys/Recursive"];
 
 use_thys ["Paper"]