diff -r 2e0203309287 -r a94ef3eed456 src/ZF/ex/Bin.thy
--- a/src/ZF/ex/Bin.thy	Tue Mar 07 13:34:33 1995 +0100
+++ b/src/ZF/ex/Bin.thy	Tue Mar 07 13:37:48 1995 +0100
@@ -18,7 +18,7 @@
 Division is not defined yet!
 *)
 
-Bin = Integ + Univ + "twos_compl" +
+Bin = Integ + Datatype + "twos_compl" +
 
 consts
   bin_rec          :: "[i, i, i, [i,i,i]=>i] => i"