src/Pure/Tools/codegen_package.ML

   val appgen_default: appgen;
   val appgen_let: (int -> term -> term list * term)
     -> appgen;
   val appgen_split: (int -> term -> term list * term)
     -> appgen;
-  val appgen_number_of: (term -> term) -> (term -> IntInf.int) -> string -> string
+  val appgen_number_of: (term -> term) -> (theory -> term -> IntInf.int) -> string -> string
     -> appgen;
   val add_case_const: (theory -> string -> (string * int) list option) -> xstring
     -> theory -> theory;
   val add_case_const_i: (theory -> string -> (string * int) list option) -> string
     -> theory -> theory;

 fun appgen_number_of mk_int_to_nat bin_to_int tyco_int tyco_nat thy tabs ((_,
   Type (_, [_, ty as Type (tyco, [])])), [bin]) trns =
     if tyco = tyco_int then
       trns
       |> exprgen_type thy tabs ty
-      |-> (fn ty => pair (CodegenThingol.IConst (((IntInf.toString o bin_to_int) bin, ty), [])))
+      |-> (fn ty => pair (CodegenThingol.IConst (((IntInf.toString o bin_to_int thy) bin, ty), [])))
     else if tyco = tyco_nat then
       trns
       |> exprgen_term thy tabs (mk_int_to_nat bin)
     else error ("invalid type constructor for numeral: " ^ quote tyco);