diff -r 64dee7d4b8ce -r 02054bf31c0e src/HOL/hologic.ML
--- a/src/HOL/hologic.ML	Thu Nov 23 00:09:24 2006 +0100
+++ b/src/HOL/hologic.ML	Thu Nov 23 00:51:47 2006 +0100
@@ -308,7 +308,7 @@
   | int_of (b :: bs) = IntInf.fromInt b + (2 * int_of bs);
 
 (*When called from a print translation, the Numeral qualifier will probably have
-  been removed from Bit, bit.B0, etc.*)
+  been removed from Bit, bit.B0, etc.*)  (* FIXME !? *)
 fun dest_bit (Const ("Numeral.bit.B0", _)) = 0
   | dest_bit (Const ("Numeral.bit.B1", _)) = 1
   | dest_bit (Const ("bit.B0", _)) = 0
@@ -323,10 +323,6 @@
 
 val dest_binum = int_of o bin_of;
 
-fun mk_bit 0 = B0_const
-  | mk_bit 1 = B1_const
-  | mk_bit _ = sys_error "mk_bit";
-
 fun mk_binum n =
   let
     fun mk_bit n = if n = 0 then B0_const else B1_const;