# HG changeset patch
# User haftmann
# Date 1138952896 -3600
# Node ID 7521b849ae980a16b6668beeafd25274b68bf88b
# Parent  5a476b10d69c15e878a97a5fd072c609abfb40a5
fix in codegen

diff -r 5a476b10d69c -r 7521b849ae98 src/HOL/Integ/IntDef.thy
--- a/src/HOL/Integ/IntDef.thy	Thu Feb 02 21:59:55 2006 +0100
+++ b/src/HOL/Integ/IntDef.thy	Fri Feb 03 08:48:16 2006 +0100
@@ -931,7 +931,7 @@
   Const ("IntDef.nat", HOLogic.intT --> HOLogic.natT)
   $ (Const ("Numeral.number_of", HOLogic.binT --> HOLogic.intT) $ bin);
 
-fun bin_to_int bin = HOLogic.dest_binum bin
+fun bin_to_int thy bin = HOLogic.dest_binum bin
   handle TERM _
     => error ("not a number: " ^ Sign.string_of_term thy bin);
 
diff -r 5a476b10d69c -r 7521b849ae98 src/Pure/Tools/codegen_package.ML
--- a/src/Pure/Tools/codegen_package.ML	Thu Feb 02 21:59:55 2006 +0100
+++ b/src/Pure/Tools/codegen_package.ML	Fri Feb 03 08:48:16 2006 +0100
@@ -41,7 +41,7 @@
     -> 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;
@@ -904,7 +904,7 @@
     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)