--- a/ROOT.ML	Fri Feb 15 07:42:47 2013 +0000
+++ b/ROOT.ML	Fri Feb 15 14:05:26 2013 +0000
@@ -3,6 +3,7 @@
 use_thys ["thys/Turing",
           "thys/Turing_Hoare", 
 	  "thys/Uncomputable", 
+          "thys/Abacus_Mopup",
 	  "thys/Abacus", 
 	  "thys/Rec_Def", 
 	  "thys/Recursive",