diff -r 1b08942bb86f -r d85a2fdc586c src/HOL/MicroJava/J/SystemClasses.thy --- a/src/HOL/MicroJava/J/SystemClasses.thy Fri Oct 21 11:17:12 2011 +0200 +++ b/src/HOL/MicroJava/J/SystemClasses.thy Fri Oct 21 11:17:14 2011 +0200 @@ -13,18 +13,18 @@ *} definition ObjectC :: "'c cdecl" where - [code_inline]: "ObjectC \ (Object, (undefined,[],[]))" + [code_unfold]: "ObjectC \ (Object, (undefined,[],[]))" definition NullPointerC :: "'c cdecl" where - [code_inline]: "NullPointerC \ (Xcpt NullPointer, (Object,[],[]))" + [code_unfold]: "NullPointerC \ (Xcpt NullPointer, (Object,[],[]))" definition ClassCastC :: "'c cdecl" where - [code_inline]: "ClassCastC \ (Xcpt ClassCast, (Object,[],[]))" + [code_unfold]: "ClassCastC \ (Xcpt ClassCast, (Object,[],[]))" definition OutOfMemoryC :: "'c cdecl" where - [code_inline]: "OutOfMemoryC \ (Xcpt OutOfMemory, (Object,[],[]))" + [code_unfold]: "OutOfMemoryC \ (Xcpt OutOfMemory, (Object,[],[]))" definition SystemClasses :: "'c cdecl list" where - [code_inline]: "SystemClasses \ [ObjectC, NullPointerC, ClassCastC, OutOfMemoryC]" + [code_unfold]: "SystemClasses \ [ObjectC, NullPointerC, ClassCastC, OutOfMemoryC]" end