| changeset 22046 | ce84c9887e2d |
| parent 21404 | eb85850d3eb7 |
| child 22190 | d31dec6397be |
--- a/src/HOL/Integ/NatBin.thy Tue Jan 09 18:13:55 2007 +0100 +++ b/src/HOL/Integ/NatBin.thy Tue Jan 09 19:08:56 2007 +0100 @@ -819,7 +819,7 @@ *} setup {* - CodegenData.add_inline_proc NumeralNat.elim_number_of_nat + CodegenData.add_inline_proc ("elim_number_of_nat", NumeralNat.elim_number_of_nat) *} subsection {* legacy ML bindings *}