--- a/src/ZF/Bin.thy Mon Feb 11 15:19:17 2008 +0100
+++ b/src/ZF/Bin.thy Mon Feb 11 15:40:21 2008 +0100
@@ -17,7 +17,7 @@
header{*Arithmetic on Binary Integers*}
theory Bin
-imports Int Datatype
+imports Int_ZF Datatype_ZF
uses "Tools/numeral_syntax.ML"
begin