
diff -r af1a0b0c6202 -r 30d512bf47a7 src/HOL/Library/Efficient_Nat.thy
--- 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)"




