# HG changeset patch
# User kleing
# Date 976202487 -3600
# Node ID f16baa9505cd506367035a710370a15f6b4ab4cc
# Parent  62a2f9d9316cfcc424c103774d3c8c9233cdf1f1
invoked class must be defined in Invoke C ...

diff -r 62a2f9d9316c -r f16baa9505cd src/HOL/MicroJava/BV/Step.thy
--- a/src/HOL/MicroJava/BV/Step.thy	Wed Dec 06 22:10:11 2000 +0100
+++ b/src/HOL/MicroJava/BV/Step.thy	Thu Dec 07 16:21:27 2000 +0100
@@ -81,7 +81,7 @@
    (let apTs = rev (take (length fpTs) (fst s));
         X    = hd (drop (length fpTs) (fst s)) 
     in  
-        G \<turnstile> X \<preceq> Class C \<and> method (G,C) (mn,fpTs) \<noteq> None \<and> 
+        G \<turnstile> X \<preceq> Class C \<and> is_class G C \<and> method (G,C) (mn,fpTs) \<noteq> None \<and> 
         (\<forall>(aT,fT)\<in>set(zip apTs fpTs). G \<turnstile> aT \<preceq> fT)))"
 
 "app' (i,G,maxs,rT,s)                             = False"
@@ -258,7 +258,7 @@
 
 lemma appInvoke[simp]:
 "app (Invoke C mn fpTs) G maxs rT (Some s) = (\<exists>apTs X ST LT mD' rT' b'.
-  s = ((rev apTs) @ (X # ST), LT) \<and> length apTs = length fpTs \<and> 
+  s = ((rev apTs) @ (X # ST), LT) \<and> length apTs = length fpTs \<and> is_class G C \<and>
   G \<turnstile> X \<preceq> Class C \<and> (\<forall>(aT,fT)\<in>set(zip apTs fpTs). G \<turnstile> aT \<preceq> fT) \<and> 
   method (G,C) (mn,fpTs) = Some (mD', rT', b'))" (is "?app s = ?P s")
 proof (cases (open) s)