diff -r 4ce22e7a81bd -r 3c243098b64a src/HOL/Tools/numeral.ML
--- a/src/HOL/Tools/numeral.ML	Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Tools/numeral.ML	Sun Feb 17 06:49:53 2008 +0100
@@ -17,15 +17,15 @@
 
 (* numeral *)
 
-fun mk_cbit 0 = @{cterm "Int.bit.B0"}
-  | mk_cbit 1 = @{cterm "Int.bit.B1"}
+fun mk_cbit 0 = @{cterm "Int.Bit0"}
+  | mk_cbit 1 = @{cterm "Int.Bit1"}
   | mk_cbit _ = raise CTERM ("mk_cbit", []);
 
 fun mk_cnumeral 0 = @{cterm "Int.Pls"}
   | mk_cnumeral ~1 = @{cterm "Int.Min"}
   | mk_cnumeral i =
       let val (q, r) = Integer.div_mod i 2 in
-        Thm.capply (Thm.capply @{cterm "Int.Bit"} (mk_cnumeral q)) (mk_cbit r)
+        Thm.capply (mk_cbit r) (mk_cnumeral q)
       end;
 
 
@@ -57,8 +57,7 @@
 
 fun add_code number_of negative unbounded target =
   CodeTarget.add_pretty_numeral target negative unbounded number_of
-  @{const_name Int.B0} @{const_name Int.B1}
   @{const_name Int.Pls} @{const_name Int.Min}
-  @{const_name Int.Bit};
+  @{const_name Int.Bit0} @{const_name Int.Bit1};
 
 end;