diff -r 4939494ed791 -r ce654b0e6d69 src/HOL/MicroJava/DFA/Kildall.thy
--- a/src/HOL/MicroJava/DFA/Kildall.thy	Tue Feb 13 14:24:50 2018 +0100
+++ b/src/HOL/MicroJava/DFA/Kildall.thy	Thu Feb 15 12:11:00 2018 +0100
@@ -203,7 +203,7 @@
      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)