src/HOL/MicroJava/JVM/JVMExec.thy

--- a/src/HOL/MicroJava/JVM/JVMExec.thy	Tue Dec 05 08:22:49 2000 +0100
+++ b/src/HOL/MicroJava/JVM/JVMExec.thy	Tue Dec 05 14:08:22 2000 +0100
@@ -19,7 +19,7 @@
 
   "exec (G, None, hp, (stk,loc,C,sig,pc)#frs) =
   (let 
-     i = snd(snd(snd(the(method (G,C) sig)))) ! pc
+     i = snd(snd(snd(snd(the(method (G,C) sig))))) ! pc
    in
      Some (exec_instr i G hp stk loc C sig pc frs))"