--- a/src/HOL/MicroJava/JVM/JVMState.thy Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/MicroJava/JVM/JVMState.thy Sat Apr 23 13:00:19 2011 +0200
@@ -12,11 +12,11 @@
begin
section {* Frame Stack *}
-types
- opstack = "val list"
- locvars = "val list"
- p_count = nat
+type_synonym opstack = "val list"
+type_synonym locvars = "val list"
+type_synonym p_count = nat
+type_synonym
frame = "opstack \<times>
locvars \<times>
cname \<times>
@@ -35,7 +35,7 @@
"raise_system_xcpt b x \<equiv> raise_if b x None"
section {* Runtime State *}
-types
+type_synonym
jvm_state = "val option \<times> aheap \<times> frame list" -- "exception flag, heap, frames"