# HG changeset patch
# User haftmann
# Date 1160464639 -7200
# Node ID 3f999b73f6d5c7f71e739e2c46f08352740e5453
# Parent  e65e1234c9d3037a623e17fdaa0e337609823ad4
added code_constsubst

diff -r e65e1234c9d3 -r 3f999b73f6d5 src/HOL/Extraction/Pigeonhole.thy
--- 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)"