diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/MicroJava/JVM/JVMInstructions.thy
--- a/src/HOL/MicroJava/JVM/JVMInstructions.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/MicroJava/JVM/JVMInstructions.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -28,13 +28,17 @@
         | Ifcmpeq int               -- "branch if int/ref comparison succeeds"
         | Throw                     -- "throw top of stack as exception"
 
-types
+type_synonym
   bytecode = "instr list"
+type_synonym
   exception_entry = "p_count \<times> p_count \<times> p_count \<times> cname" 
                   -- "start-pc, end-pc, handler-pc, exception type"
+type_synonym
   exception_table = "exception_entry list"
+type_synonym
   jvm_method = "nat \<times> nat \<times> bytecode \<times> exception_table"
    -- "max stacksize, size of register set, instruction sequence, handler table"
+type_synonym
   jvm_prog = "jvm_method prog" 
 
 end