--- a/src/HOL/MicroJava/BV/BVExample.thy Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/MicroJava/BV/BVExample.thy Mon Dec 28 17:43:30 2015 +0100
@@ -424,7 +424,7 @@
apply (case_tac "\<not> stable r step ss p")
apply simp_all
done
- also have "\<And>f. (UN p:{..<size ss}. f p) = Union (set (map f [0..<size ss]))" by auto
+ 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 {}) =
(\<lambda>p A. if \<not>stable r step ss p then insert p A else A)"