# HG changeset patch
# User kleing
# Date 965651643 -7200
# Node ID 19a6d1289f5ea458ced4a58fddbc14b56225166b
# Parent  40d64cb4f4e63b471f478703be47107cc1c71589
Invoke instruction gets fully qualified method name (class+name+sig) as
in Sun's JVM spec

diff -r 40d64cb4f4e6 -r 19a6d1289f5e src/HOL/MicroJava/JVM/JVMExecInstr.thy
--- a/src/HOL/MicroJava/JVM/JVMExecInstr.thy	Mon Aug 07 14:32:56 2000 +0200
+++ b/src/HOL/MicroJava/JVM/JVMExecInstr.thy	Mon Aug 07 14:34:03 2000 +0200
@@ -56,7 +56,7 @@
 	 in
       (xp', hp, (stk', vars, Cl, sig, pc+1)#frs))"
 
- "exec_instr (Invoke mn ps) G hp stk vars Cl sig pc frs =
+ "exec_instr (Invoke C mn ps) G hp stk vars Cl sig pc frs =
 	(let n		= length ps;
 	     argsoref	= take (n+1) stk;
 	     oref	= last argsoref;
diff -r 40d64cb4f4e6 -r 19a6d1289f5e src/HOL/MicroJava/JVM/JVMInstructions.thy
--- a/src/HOL/MicroJava/JVM/JVMInstructions.thy	Mon Aug 07 14:32:56 2000 +0200
+++ b/src/HOL/MicroJava/JVM/JVMInstructions.thy	Mon Aug 07 14:34:03 2000 +0200
@@ -8,6 +8,7 @@
 
 JVMInstructions = JVMState +
 
+
 datatype 
   instr = Load nat                  (* load from local variable *)
         | Store nat                 (* store into local variable *)
@@ -17,7 +18,7 @@
         | Getfield vname cname	  	(* Fetch field from object *)
         | Putfield vname cname		  (* Set field in object     *)
         | Checkcast cname	          (* Check whether object is of given type *)
-        | Invoke mname "(ty list)"  (* inv. instance meth of an object *)
+        | Invoke cname mname "(ty list)"  (* inv. instance meth of an object *)
         | Return
         | Pop
         | Dup