src/ZF/ex/ROOT.ML

--- a/src/ZF/ex/ROOT.ML	Tue Sep 22 15:24:01 1998 +0200
+++ b/src/ZF/ex/ROOT.ML	Tue Sep 22 15:24:39 1998 +0200
@@ -15,9 +15,7 @@
 time_use_thy "Primes";          (*GCD theory*)
 time_use_thy "Ramsey";          (*Simple form of Ramsey's theorem*)
 time_use_thy "Limit";           (*Inverse limit construction of domains*)
-
-(*Integers & Binary integer arithmetic*)
-time_use_thy "Bin";
+time_use     "BinEx";		(*Binary integer arithmetic*)
 
 (** Datatypes **)
 time_use_thy "BT";              (*binary trees*)