--- a/src/HOL/MicroJava/J/JListExample.thy Fri Oct 21 11:17:12 2011 +0200
+++ b/src/HOL/MicroJava/J/JListExample.thy Fri Oct 21 11:17:14 2011 +0200
@@ -118,12 +118,12 @@
definition undefined_cname :: cname
where [code del]: "undefined_cname = undefined"
-declare undefined_cname_def[symmetric, code_inline]
+declare undefined_cname_def[symmetric, code_unfold]
code_datatype Object Xcpt Cname undefined_cname
definition undefined_val :: val
where [code del]: "undefined_val = undefined"
-declare undefined_val_def[symmetric, code_inline]
+declare undefined_val_def[symmetric, code_unfold]
code_datatype Unit Null Bool Intg Addr undefined_val
definition E where