diff -r 64ab5bb68d4c -r bd8438543bf2 src/HOL/Tools/numeral.ML
--- a/src/HOL/Tools/numeral.ML	Wed Oct 22 14:15:44 2008 +0200
+++ b/src/HOL/Tools/numeral.ML	Wed Oct 22 14:15:45 2008 +0200
@@ -59,25 +59,28 @@
 
 fun add_code number_of negative unbounded target thy =
   let
-    val pls' = Code_Name.const thy @{const_name Int.Pls};
-    val min' = Code_Name.const thy @{const_name Int.Min};
-    val bit0' = Code_Name.const thy @{const_name Int.Bit0};
-    val bit1' = Code_Name.const thy @{const_name Int.Bit1};
     val pr_numeral = (Code_Printer.literal_numeral o Code_Target.the_literals thy) target;
-    fun dest_bit thm (IConst (c, _)) = if c = bit0' then 0
-          else if c = bit1' then 1
-          else Code_Printer.nerror thm "Illegal numeral expression: illegal bit"
-      | dest_bit thm _ = Code_Printer.nerror thm "Illegal numeral expression: illegal bit";
-    fun dest_numeral thm (IConst (c, _)) = if c = pls' then SOME 0
-          else if c = min' then
-            if negative then SOME ~1 else NONE
-          else Code_Printer.nerror thm "Illegal numeral expression: illegal leading digit"
-      | dest_numeral thm (t1 `$ t2) =
-          let val (n, b) = (dest_numeral thm t2, dest_bit thm t1)
-          in case n of SOME n => SOME (2 * n + b) | NONE => NONE end
-      | dest_numeral thm _ = Code_Printer.nerror thm "Illegal numeral expression: illegal term";
-    fun pretty _ thm _ _ _ [(t, _)] =
-      (Code_Printer.str o pr_numeral unbounded o the_default 0 o dest_numeral thm) t;
+    fun dest_numeral naming thm =
+      let
+        val SOME pls' = Code_Thingol.lookup_const naming @{const_name Int.Pls};
+        val SOME min' = Code_Thingol.lookup_const naming @{const_name Int.Min};
+        val SOME bit0' = Code_Thingol.lookup_const naming @{const_name Int.Bit0};
+        val SOME bit1' = Code_Thingol.lookup_const naming @{const_name Int.Bit1};
+        fun dest_bit (IConst (c, _)) = if c = bit0' then 0
+              else if c = bit1' then 1
+              else Code_Printer.nerror thm "Illegal numeral expression: illegal bit"
+          | dest_bit _ = Code_Printer.nerror thm "Illegal numeral expression: illegal bit";
+        fun dest_num (IConst (c, _)) = if c = pls' then SOME 0
+              else if c = min' then
+                if negative then SOME ~1 else NONE
+              else Code_Printer.nerror thm "Illegal numeral expression: illegal leading digit"
+          | dest_num (t1 `$ t2) =
+              let val (n, b) = (dest_num t2, dest_bit t1)
+              in case n of SOME n => SOME (2 * n + b) | NONE => NONE end
+          | dest_num _ = Code_Printer.nerror thm "Illegal numeral expression: illegal term";
+      in dest_num end;
+    fun pretty _ naming thm _ _ _ [(t, _)] =
+      (Code_Printer.str o pr_numeral unbounded o the_default 0 o dest_numeral naming thm) t;
   in
     thy
     |> Code_Target.add_syntax_const target number_of (SOME (1, pretty))