--- a/src/HOL/MicroJava/BV/BVExample.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/MicroJava/BV/BVExample.thy Wed Jan 10 15:25:09 2018 +0100
@@ -426,7 +426,7 @@
done
also have "\<And>f. (UN p:{..<size ss}. f p) = \<Union>(set (map f [0..<size ss]))" by auto
also note Sup_set_fold also note fold_map
- also have "op \<union> \<circ> (\<lambda>p. if \<not> stable r step ss p then {p} else {}) =
+ also have "(\<union>) \<circ> (\<lambda>p. if \<not> stable r step ss p then {p} else {}) =
(\<lambda>p A. if \<not>stable r step ss p then insert p A else A)"
by(auto simp add: fun_eq_iff)
finally show ?thesis .