diff -r 876dd2695423 -r 3c5074f028c8 src/HOL/MicroJava/JVM/JVMListExample.thy
--- a/src/HOL/MicroJava/JVM/JVMListExample.thy	Fri Oct 20 10:44:39 2006 +0200
+++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Fri Oct 20 10:44:42 2006 +0200
@@ -120,22 +120,20 @@
   and vname :: eq
   and mname :: eq
   and ty :: eq
+  and val :: eq
   and instr :: eq ..
 
 definition
   arbitrary_val :: val
-  "arbitrary_val = arbitrary"
+  [symmetric, code inline]: "arbitrary_val = arbitrary"
   arbitrary_cname :: cname
-  "arbitrary_cname = arbitrary"
-
-declare arbitrary_val_def [symmetric, code inline]
-declare arbitrary_cname_def [symmetric, code inline]
+  [symmetric, code inline]: "arbitrary_cname = arbitrary"
 
 definition
   "unit' = Unit"
   "object' = Object"
 
-code_constsubst
+code_axioms
   arbitrary_val \<equiv> unit'
   arbitrary_cname \<equiv> object'
 
@@ -165,7 +163,7 @@
 code_const
   wf_class (SML target_atom "(fn _ => true)")
 
-code_constsubst
+code_axioms
   new_Addr \<equiv> new_addr'
 
 definition