diff -r ef1e0cb80fde -r 949d93804740 src/HOL/MicroJava/DFA/LBVCorrect.thy
--- a/src/HOL/MicroJava/DFA/LBVCorrect.thy	Tue May 22 14:12:15 2018 +0200
+++ b/src/HOL/MicroJava/DFA/LBVCorrect.thy	Tue May 22 11:08:37 2018 +0200
@@ -88,7 +88,7 @@
     also    
     from s2 merge have "\<dots> \<noteq> \<top>" (is "?merge \<noteq> _") by simp
     with cert_in_A step_in_A
-    have "?merge = (map snd [(p',t') \<leftarrow> ?step pc. p'=pc+1] ++_f (c!(pc+1)))"
+    have "?merge = (map snd (filter (\<lambda>(p',t').p'=pc+1) (?step pc)) ++_f (c!(pc+1)))"
       by (rule merge_not_top_s) 
     finally
     have "s' <=_r ?s2" using step_in_A cert_in_A True step