--- a/src/HOL/Extraction/Pigeonhole.thy Fri Oct 20 10:44:38 2006 +0200
+++ b/src/HOL/Extraction/Pigeonhole.thy Fri Oct 20 10:44:39 2006 +0200
@@ -303,16 +303,14 @@
definition
arbitrary_nat :: "nat \<times> nat"
- "arbitrary_nat = arbitrary"
+ [symmetric, code inline]: "arbitrary_nat = arbitrary"
arbitrary_nat_subst :: "nat \<times> nat"
"arbitrary_nat_subst = (0, 0)"
lemma [code func]:
"arbitrary_nat = arbitrary_nat" ..
-declare arbitrary_nat_def [symmetric, code inline]
-
-code_constsubst
+code_axioms
arbitrary_nat \<equiv> arbitrary_nat_subst
definition