1.1 --- a/src/HOL/MicroJava/JVM/JVMState.thy	Thu Nov 25 12:30:57 1999 +0100
     1.2 +++ b/src/HOL/MicroJava/JVM/JVMState.thy	Fri Nov 26 08:46:59 1999 +0100
     1.3 @@ -35,21 +35,10 @@
     1.4   raise_xcpt :: "bool \\<Rightarrow> xcpt \\<Rightarrow> xcpt option"
     1.5  "raise_xcpt c x \\<equiv> (if c then Some x else None)"
     1.6  
     1.7 - heap_update :: "[xcpt option,aheap,aheap] \\<Rightarrow> aheap"
     1.8 -"heap_update xp hp' hp \\<equiv> if xp=None then hp' else hp"
     1.9 -
    1.10 - stk_update :: "[xcpt option,opstack,opstack] \\<Rightarrow> opstack"
    1.11 -"stk_update xp stk' stk \\<equiv> if xp=None then stk' else stk"
    1.12 -
    1.13 - xcpt_update :: "[xcpt option,'a,'a] \\<Rightarrow> 'a"
    1.14 -"xcpt_update xp y' y \\<equiv> if xp=None then y' else y"
    1.15 -
    1.16  (** runtime state **)
    1.17  
    1.18  types
    1.19 - jvm_state = "xcpt option \\<times>		
    1.20 -	      aheap \\<times>				
    1.21 -	      frame list"	
    1.22 + jvm_state = "xcpt option \\<times> aheap \\<times> frame list"	
    1.23  
    1.24  
    1.25  
    1.26 @@ -57,5 +46,5 @@
    1.27  
    1.28  constdefs
    1.29   dyn_class	:: "'code prog \\<times> sig \\<times> cname \\<Rightarrow> cname"
    1.30 -"dyn_class \\<equiv> \\<lambda>(G,sig,C). fst(the(cmethd(G,C) sig))"
    1.31 +"dyn_class \\<equiv> \\<lambda>(G,sig,C). fst(the(method(G,C) sig))"
    1.32  end