--- a/src/HOL/Extraction/Pigeonhole.thy Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Extraction/Pigeonhole.thy Fri Nov 17 02:20:03 2006 +0100
@@ -302,9 +302,10 @@
ML "PH.pigeonhole 8 (PH.sel [0,1,2,3,4,5,6,3,7,8])"
definition
- arbitrary_nat :: "nat \<times> nat"
+ arbitrary_nat :: "nat \<times> nat" where
[symmetric, code inline]: "arbitrary_nat = arbitrary"
- arbitrary_nat_subst :: "nat \<times> nat"
+definition
+ arbitrary_nat_subst :: "nat \<times> nat" where
"arbitrary_nat_subst = (0, 0)"
code_axioms
@@ -312,6 +313,7 @@
definition
"test n = pigeonhole n (\<lambda>m. m - 1)"
+definition
"test' n = pigeonhole_slow n (\<lambda>m. m - 1)"
code_gen test test' "op !" (SML *)