src/HOL/NanoJava/Decl.thy
changeset 18551 be0705186ff5
parent 16417 9bc16273c2d4
child 32960 69916a850301
--- 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 \<times> methd"
 
-record	class
+record	"class"
 	= super   :: cname
           flds    ::"fdecl list"
           methods ::"mdecl list"
@@ -52,7 +52,7 @@
 
 
 constdefs
-  class	     :: "cname \<rightharpoonup> class"
+  "class"	     :: "cname \<rightharpoonup> class"
  "class      \<equiv> map_of Prog"
 
   is_class   :: "cname => bool"