diff -r 23386a5b63eb -r 697fab84709e src/HOL/MicroJava/JVM/JVMExecInstr.thy
--- 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