| changeset 22921 | 475ff421a6a3 |
| parent 22845 | 5f9138bcb3d7 |
| child 23810 | f5e6932d0500 |
--- a/src/HOL/Extraction/Pigeonhole.thy Thu May 10 10:21:50 2007 +0200 +++ b/src/HOL/Extraction/Pigeonhole.thy Thu May 10 10:22:17 2007 +0200 @@ -293,7 +293,7 @@ consts_code - arbitrary :: "nat \<times> nat" ("{* (0::nat, 0::nat) *}") + "arbitrary :: nat \<times> nat" ("{* (0::nat, 0::nat) *}") definition arbitrary_nat_pair :: "nat \<times> nat" where