diff -r 53a081c8873d -r 322d1657c40c src/HOL/MicroJava/J/SystemClasses.thy --- a/src/HOL/MicroJava/J/SystemClasses.thy Fri Aug 05 00:14:08 2011 +0200 +++ b/src/HOL/MicroJava/J/SystemClasses.thy Fri Aug 05 14:16:44 2011 +0200 @@ -13,18 +13,18 @@ *} definition ObjectC :: "'c cdecl" where - "ObjectC \ (Object, (undefined,[],[]))" + [code_inline]: "ObjectC \ (Object, (undefined,[],[]))" definition NullPointerC :: "'c cdecl" where - "NullPointerC \ (Xcpt NullPointer, (Object,[],[]))" + [code_inline]: "NullPointerC \ (Xcpt NullPointer, (Object,[],[]))" definition ClassCastC :: "'c cdecl" where - "ClassCastC \ (Xcpt ClassCast, (Object,[],[]))" + [code_inline]: "ClassCastC \ (Xcpt ClassCast, (Object,[],[]))" definition OutOfMemoryC :: "'c cdecl" where - "OutOfMemoryC \ (Xcpt OutOfMemory, (Object,[],[]))" + [code_inline]: "OutOfMemoryC \ (Xcpt OutOfMemory, (Object,[],[]))" definition SystemClasses :: "'c cdecl list" where - "SystemClasses \ [ObjectC, NullPointerC, ClassCastC, OutOfMemoryC]" + [code_inline]: "SystemClasses \ [ObjectC, NullPointerC, ClassCastC, OutOfMemoryC]" end