--- a/src/HOL/MicroJava/J/Decl.thy Wed Mar 03 00:32:14 2010 +0100
+++ b/src/HOL/MicroJava/J/Decl.thy Wed Mar 03 00:33:02 2010 +0100
@@ -23,12 +23,12 @@
translations
- "fdecl" <= (type) "vname \<times> ty"
- "sig" <= (type) "mname \<times> ty list"
- "mdecl c" <= (type) "sig \<times> ty \<times> c"
- "class c" <= (type) "cname \<times> fdecl list \<times> (c mdecl) list"
- "cdecl c" <= (type) "cname \<times> (c class)"
- "prog c" <= (type) "(c cdecl) list"
+ (type) "fdecl" <= (type) "vname \<times> ty"
+ (type) "sig" <= (type) "mname \<times> ty list"
+ (type) "'c mdecl" <= (type) "sig \<times> ty \<times> 'c"
+ (type) "'c class" <= (type) "cname \<times> fdecl list \<times> ('c mdecl) list"
+ (type) "'c cdecl" <= (type) "cname \<times> ('c class)"
+ (type) "'c prog" <= (type) "('c cdecl) list"
definition "class" :: "'c prog => (cname \<rightharpoonup> 'c class)" where