diff -r b3d18eb3ac20 -r 2497807020fa src/HOL/ROOT.ML
--- a/src/HOL/ROOT.ML	Wed Jul 01 19:11:20 1998 +0200
+++ b/src/HOL/ROOT.ML	Thu Jul 02 16:44:39 1998 +0200
@@ -57,7 +57,7 @@
 use_thy "Update";
 
 cd "Integ";
-use "ROOT.ML";
+use_thy "Bin";
 cd "..";
 
 (*TFL: recursive function definitions*)