src/HOL/Bali/Decl.thy

 record cbody = decl +          --{* class body *}
          cfields:: "fdecl list" 
          methods:: "mdecl list"
          init   :: "stmt"       --{* initializer *}
 
-record class = cbody +           --{* class *}
+record "class" = cbody +           --{* class *}
         super   :: "qtname"      --{* superclass *}
         superIfs:: "qtname list" --{* implemented interfaces *}
 types	
 	cdecl           --{* class declaration, cf. 8.1 *}
 	= "qtname \<times> class"

      "prog"<= (type) "\<lparr>ifaces::idecl list,classes::cdecl list\<rparr>"
      "prog"<= (type) "\<lparr>ifaces::idecl list,classes::cdecl list,\<dots>::'a\<rparr>"
 
 syntax
   iface     :: "prog  \<Rightarrow> (qtname, iface) table"
-  class     :: "prog  \<Rightarrow> (qtname, class) table"
+  "class"     :: "prog  \<Rightarrow> (qtname, class) table"
   is_iface  :: "prog  \<Rightarrow> qtname  \<Rightarrow> bool"
   is_class  :: "prog  \<Rightarrow> qtname  \<Rightarrow> bool"
 
 translations
 	   "iface G I" == "table_of (ifaces G) I"