src/HOL/MicroJava/DFA/Kildall.thy

      \<forall>q. q < n \<longrightarrow> q \<notin> w \<longrightarrow> stable r step ss q; q < n; 
      \<forall>s'. (q,s') \<in> set (step p (ss ! p)) \<longrightarrow> s' +_f ss ! q = ss ! q; 
      q \<notin> w \<or> q = p \<rbrakk> 
   \<Longrightarrow> stable r step (merges f (step p (ss!p)) ss) q"
   apply (unfold stable_def)
-  apply (subgoal_tac "\<forall>s'. (q,s') \<in> set (step p (ss!p)) \<longrightarrow> s' : A")
+  apply (subgoal_tac "\<forall>s'. (q,s') \<in> set (step p (ss!p)) \<longrightarrow> s' \<in> A")
    prefer 2
    apply clarify
    apply (erule pres_typeD)
     prefer 3 apply assumption
     apply (rule listE_nth_in)