src/HOL/Extraction/Pigeonhole.thy
changeset 20933 3f999b73f6d5
parent 20837 099877d83d2b
child 21062 876dd2695423
--- a/src/HOL/Extraction/Pigeonhole.thy	Tue Oct 10 09:17:18 2006 +0200
+++ b/src/HOL/Extraction/Pigeonhole.thy	Tue Oct 10 09:17:19 2006 +0200
@@ -304,14 +304,16 @@
 definition
   arbitrary_nat :: "nat \<times> nat"
   "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_const arbitrary_nat
-  (SML "{* (0\<Colon>nat, 0\<Colon>nat) *}")
+code_constsubst
+  arbitrary_nat \<equiv> arbitrary_nat_subst
 
 definition
   "test n = pigeonhole n (\<lambda>m. m - 1)"