diff -r 23386a5b63eb -r 697fab84709e src/HOL/MicroJava/BV/StepMono.thy
--- a/src/HOL/MicroJava/BV/StepMono.thy	Sun Jan 14 18:17:37 2001 +0100
+++ b/src/HOL/MicroJava/BV/StepMono.thy	Sun Jan 14 18:19:18 2001 +0100
@@ -143,11 +143,7 @@
         by - (cases s2, auto simp add: map_eq_Cons sup_loc_Cons2 
                                        sup_loc_length sup_state_conv)
     next
-      case Bipush
-      with G app
-      show ?thesis by simp 
-    next
-      case Aconst_null
+      case LitPush
       with G app
       show ?thesis by simp
     next
@@ -355,7 +351,7 @@
     show ?thesis
       by (clarsimp simp add: sup_state_conv sup_loc_update)
   next
-    case Bipush
+    case LitPush
     with G s step app1 app2
     show ?thesis
       by (clarsimp simp add: sup_state_Cons1)
@@ -365,11 +361,6 @@
     show ?thesis
       by (clarsimp simp add: sup_state_Cons1)
   next
-    case Aconst_null
-    with G s step app1 app2
-    show ?thesis
-      by (clarsimp simp add: sup_state_Cons1)
-  next
     case Getfield
     with G s step app1 app2
     show ?thesis