--- a/src/HOL/MicroJava/JVM/JVMExecInstr.thy Sun Jan 14 18:17:37 2001 +0100
+++ b/src/HOL/MicroJava/JVM/JVMExecInstr.thy Sun Jan 14 18:19:18 2001 +0100
@@ -21,16 +21,13 @@
"exec_instr (Store idx) G hp stk vars Cl sig pc frs =
(None, hp, (tl stk, vars[idx:=hd stk], Cl, sig, pc+1)#frs)"
- "exec_instr (Bipush ival) G hp stk vars Cl sig pc frs =
- (None, hp, (Intg ival # stk, vars, Cl, sig, pc+1)#frs)"
-
- "exec_instr Aconst_null G hp stk vars Cl sig pc frs =
- (None, hp, (Null # stk, vars, Cl, sig, pc+1)#frs)"
+ "exec_instr (LitPush v) G hp stk vars Cl sig pc frs =
+ (None, hp, (v # stk, vars, Cl, sig, pc+1)#frs)"
"exec_instr (New C) G hp stk vars Cl sig pc frs =
(let xp' = raise_xcpt (\<forall>x. hp x \<noteq> None) OutOfMemory;
oref = newref hp;
- fs = init_vars (fields(G,C));
+ fs = init_vars (fields(G,C));
hp' = if xp'=None then hp(oref \<mapsto> (C,fs)) else hp;
stk' = if xp'=None then (Addr oref)#stk else stk
in