diff -r 59b89f625d68 -r be0705186ff5 src/HOL/NanoJava/Decl.thy --- a/src/HOL/NanoJava/Decl.thy Tue Jan 03 11:32:16 2006 +0100 +++ b/src/HOL/NanoJava/Decl.thy Tue Jan 03 11:32:55 2006 +0100 @@ -26,7 +26,7 @@ types mdecl = "mname \ methd" -record class +record "class" = super :: cname flds ::"fdecl list" methods ::"mdecl list" @@ -52,7 +52,7 @@ constdefs - class :: "cname \ class" + "class" :: "cname \ class" "class \ map_of Prog" is_class :: "cname => bool"