diff -r 91d5ac5ebb17 -r 31847a7504ec src/ZF/ex/Bin.thy
--- a/src/ZF/ex/Bin.thy	Wed Sep 07 13:04:28 1994 +0200
+++ b/src/ZF/ex/Bin.thy	Wed Sep 07 17:28:53 1994 +0200
@@ -6,7 +6,7 @@
 Arithmetic on binary integers.
 *)
 
-Bin = Integ + Univ + 
+Bin = Integ + Univ + "twos_compl" +
 consts
   bin_rec          :: "[i, i, i, [i,i,i]=>i] => i"
   integ_of_bin     :: "i=>i"