diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/MicroJava/J/Decl.thy
--- a/src/HOL/MicroJava/J/Decl.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/MicroJava/J/Decl.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -7,18 +7,23 @@
 
 theory Decl imports Type begin
 
-types 
+type_synonym 
   fdecl    = "vname \<times> ty"        -- "field declaration, cf. 8.3 (, 9.3)"
 
+type_synonym
   sig      = "mname \<times> ty list"   -- "signature of a method, cf. 8.4.2"
 
+type_synonym
   'c mdecl = "sig \<times> ty \<times> 'c"     -- "method declaration in a class"
 
+type_synonym
   'c "class" = "cname \<times> fdecl list \<times> 'c mdecl list" 
   -- "class = superclass, fields, methods"
 
+type_synonym
   'c cdecl = "cname \<times> 'c class"  -- "class declaration, cf. 8.1"
 
+type_synonym
   'c prog  = "'c cdecl list"     -- "program"