diff -r 527563e67194 -r 5af400cc64d5 src/HOL/Extraction/Pigeonhole.thy
--- a/src/HOL/Extraction/Pigeonhole.thy	Tue Sep 19 15:21:51 2006 +0200
+++ b/src/HOL/Extraction/Pigeonhole.thy	Tue Sep 19 15:21:52 2006 +0200
@@ -285,6 +285,9 @@
 consts_code
   arbitrary :: "nat \<times> nat" ("{* (0::nat, 0::nat) *}")
 
+code_const "arbitrary \<Colon> nat \<times> nat"
+  (SML "{* (0\<Colon>nat, 0\<Colon>nat) *}")
+
 code_module PH
 contains
   test = "\<lambda>n. pigeonhole n (\<lambda>m. m - 1)"