src/HOL/Tools/numeral.ML

           | 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, _)] =
+    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))
   end;