# HG changeset patch
# User kleing
# Date 976202507 -3600
# Node ID 850fdf9ce787d8a1c8e525476dbd1e1ecab0d437
# Parent  f16baa9505cd506367035a710370a15f6b4ab4cc
update for changes in Step.thy

diff -r f16baa9505cd -r 850fdf9ce787 src/HOL/MicroJava/BV/StepMono.thy
--- a/src/HOL/MicroJava/BV/StepMono.thy	Thu Dec 07 16:21:27 2000 +0100
+++ b/src/HOL/MicroJava/BV/StepMono.thy	Thu Dec 07 16:21:47 2000 +0100
@@ -250,10 +250,11 @@
       obtain apTs X ST LT mD' rT' b' where
         s1: "s1 = (rev apTs @ X # ST, LT)" and
         l:  "length apTs = length list" and
+        c:  "is_class G cname" and
         C:  "G \<turnstile> X \<preceq> Class cname" and
         w:  "\<forall>x \<in> set (zip apTs list). x \<in> widen G" and
         m:  "method (G, cname) (mname, list) = Some (mD', rT', b')"
-        by (simp, elim exE conjE) (rule that)
+        by (simp del: not_None_eq, elim exE conjE) (rule that)
 
       obtain apTs' X' ST' LT' where
         s2: "s2 = (rev apTs' @ X' # ST', LT')" and
@@ -295,7 +296,7 @@
       have w': "\<forall>x \<in> set (zip apTs' list). x \<in> widen G"
         by (simp add: all_widen_is_sup_loc)
 
-      from Invoke s2 l' w' C' m
+      from Invoke s2 l' w' C' m c
       show ?thesis
         by (simp del: split_paired_Ex) blast
     qed