--- 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"