diff -r df2862dc23a8 -r 8758fe1fc9f8 src/HOL/MicroJava/J/Decl.thy
--- 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