# HG changeset patch
# User haftmann
# Date 1161333879 -7200
# Node ID 876dd269542363e97f99faeee5998c363fad8e3e
# Parent  580dfc999ef6b352916ee9a211d4e41746083b44
slight adaption

diff -r 580dfc999ef6 -r 876dd2695423 src/HOL/Extraction/Pigeonhole.thy
--- 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
diff -r 580dfc999ef6 -r 876dd2695423 src/Pure/Tools/codegen_package.ML
--- a/src/Pure/Tools/codegen_package.ML	Fri Oct 20 10:44:38 2006 +0200
+++ b/src/Pure/Tools/codegen_package.ML	Fri Oct 20 10:44:39 2006 +0200
@@ -656,8 +656,8 @@
     (map (serialize' cs code) seris'; ())
   end;
 
-val (codeK, code_abstypeK, code_constsubstK) =
-  ("code_gen", "code_abstype", "code_constsubst");
+val (codeK, code_abstypeK, code_axiomsK) =
+  ("code_gen", "code_abstype", "code_axioms");
 
 in
 
@@ -677,13 +677,13 @@
     >> (Toplevel.theory o uncurry abstyp_e)
   );
 
-val code_constsubstP =
-  OuterSyntax.command code_constsubstK "axiomatic constant substitutions for code generation" K.thy_decl (
+val code_axiomsP =
+  OuterSyntax.command code_axiomsK "axiomatic constant equalities for code generation" K.thy_decl (
     Scan.repeat1 (P.term --| (P.$$$ "\\<equiv>" || P.$$$ "==") -- P.term)
     >> (Toplevel.theory o constsubst_e)
   );
 
-val _ = OuterSyntax.add_parsers [codeP, code_abstypeP, code_constsubstP];
+val _ = OuterSyntax.add_parsers [codeP, code_abstypeP, code_axiomsP];
 
 end; (* local *)