--- a/src/HOL/MicroJava/JVM/JVMInstructions.thy Sun Jan 14 18:17:37 2001 +0100
+++ b/src/HOL/MicroJava/JVM/JVMInstructions.thy Sun Jan 14 18:19:18 2001 +0100
@@ -13,8 +13,7 @@
datatype
instr = Load nat (* load from local variable *)
| Store nat (* store into local variable *)
- | Bipush int (* push int *)
- | Aconst_null (* push null *)
+ | LitPush val (* push a literal (constant) *)
| New cname (* create object *)
| Getfield vname cname (* Fetch field from object *)
| Putfield vname cname (* Set field in object *)