src/HOL/MicroJava/JVM/JVMExec.thy

 
 (** exec is not recursive. recdef is just used because for pattern matching **)
 recdef exec "{}"
  "exec (G, xp, hp, []) = None"
 
- "exec (G, None, hp, (stk,loc,cn,ml,pc)#frs) = 
-   Some (case snd(snd(snd(the(method (G,cn) ml)))) ! pc of
+ "exec (G, None, hp, (stk,loc,C,sig,pc)#frs) =
+   Some (case snd(snd(snd(the(method (G,C) sig)))) ! pc of
       LS ins \\<Rightarrow> let (stk',loc',pc') = exec_las ins stk loc pc
 		in
-		(None,hp,(stk',loc',cn,ml,pc')#frs)
+		(None,hp,(stk',loc',C,sig,pc')#frs)
 
     | CO ins \\<Rightarrow> let (xp',hp',stk',pc') = exec_co ins G hp stk pc
 		in
-		(xp',hp',(stk',loc,cn,ml,pc')#frs)	    
+		(xp',hp',(stk',loc,C,sig,pc')#frs)	    
 
     | MO ins \\<Rightarrow> let (xp',hp',stk',pc') = exec_mo ins hp stk pc
 		in
-		(xp',hp',(stk',loc,cn,ml,pc')#frs)
+		(xp',hp',(stk',loc,C,sig,pc')#frs)
 
     | CH ins \\<Rightarrow> let (xp',stk',pc') = exec_ch ins G hp stk pc
 		in
-		(xp',hp,(stk',loc,cn,ml,pc')#frs)
+		(xp',hp,(stk',loc,C,sig,pc')#frs)
 
     | MI ins \\<Rightarrow> let (xp',frs',stk',pc') = exec_mi ins G hp stk pc 
 		in
-		(xp',hp,frs'@(stk',loc,cn,ml,pc')#frs)
+		(xp',hp,frs'@(stk',loc,C,sig,pc')#frs)
 
     | MR ins \\<Rightarrow> let frs' = exec_mr ins stk frs in (None,hp,frs')
 
     | OS ins \\<Rightarrow> let (stk',pc') = exec_os ins stk pc
 		in
-		(None,hp,(stk',loc,cn,ml,pc')#frs)
+		(None,hp,(stk',loc,C,sig,pc')#frs)
 
     | BR ins \\<Rightarrow> let (stk',pc') = exec_br ins stk pc
 		in
-		(None,hp,(stk',loc,cn,ml,pc')#frs))"
+		(None,hp,(stk',loc,C,sig,pc')#frs))"
 
- "exec (G, Some xp, hp, f#frs) = None"
+ "exec (G, Some xp, hp, frs) = None"
 
 
 constdefs
  exec_all :: "[jvm_prog,jvm_state,jvm_state] \\<Rightarrow> bool"  ("_ \\<turnstile> _ -jvm\\<rightarrow> _" [61,61,61]60)
  "G \\<turnstile> s -jvm\\<rightarrow> t \\<equiv> (s,t) \\<in> {(s,t). exec(G,s) = Some t}^*"