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