--- a/src/HOL/Library/Efficient_Nat.thy Thu Nov 18 17:01:16 2010 +0100
+++ b/src/HOL/Library/Efficient_Nat.thy Thu Nov 18 17:01:16 2010 +0100
@@ -51,8 +51,8 @@
unfolding of_nat_mult [symmetric] by simp
lemma divmod_nat_code [code]:
- "divmod_nat n m = prod_fun nat nat (pdivmod (of_nat n) (of_nat m))"
- by (simp add: prod_fun_def split_def pdivmod_def nat_div_distrib nat_mod_distrib divmod_nat_div_mod)
+ "divmod_nat n m = map_pair nat nat (pdivmod (of_nat n) (of_nat m))"
+ by (simp add: map_pair_def split_def pdivmod_def nat_div_distrib nat_mod_distrib divmod_nat_div_mod)
lemma eq_nat_code [code]:
"HOL.equal n m \<longleftrightarrow> HOL.equal (of_nat n \<Colon> int) (of_nat m)"