diff -r 59b89f625d68 -r be0705186ff5 src/HOL/MicroJava/J/Decl.thy
--- a/src/HOL/MicroJava/J/Decl.thy	Tue Jan 03 11:32:16 2006 +0100
+++ b/src/HOL/MicroJava/J/Decl.thy	Tue Jan 03 11:32:55 2006 +0100
@@ -15,7 +15,7 @@
 
   'c mdecl = "sig \<times> ty \<times> 'c"     -- "method declaration in a class"
 
-  'c class = "cname \<times> fdecl list \<times> 'c mdecl list" 
+  'c "class" = "cname \<times> fdecl list \<times> 'c mdecl list" 
   -- "class = superclass, fields, methods"
 
   'c cdecl = "cname \<times> 'c class"  -- "class declaration, cf. 8.1"
@@ -33,7 +33,7 @@
 
 
 constdefs
-  class :: "'c prog => (cname \<rightharpoonup> 'c class)"
+  "class" :: "'c prog => (cname \<rightharpoonup> 'c class)"
   "class \<equiv> map_of"
 
   is_class :: "'c prog => cname => bool"