--- 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