diff -r 5c579bb9adb1 -r 98cf1c823c48 src/HOL/MicroJava/DFA/LBVCorrect.thy
--- a/src/HOL/MicroJava/DFA/LBVCorrect.thy	Sun Jun 03 19:06:56 2018 +0200
+++ b/src/HOL/MicroJava/DFA/LBVCorrect.thy	Wed Jun 06 11:12: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 (filter (\<lambda>(p',t').p'=pc+1) (?step pc)) ++_f (c!(pc+1)))"
+    have "?merge = (map snd [(p',t') \<leftarrow> ?step pc. p'=pc+1] ++_f (c!(pc+1)))"
       by (rule merge_not_top_s) 
     finally
     have "s' <=_r ?s2" using step_in_A cert_in_A True step