--- a/src/HOL/Transitive_Closure.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Transitive_Closure.thy Wed Feb 17 21:51:56 2016 +0100
@@ -946,7 +946,7 @@
apply (rule iffI)
apply (drule tranclD2)
apply (clarsimp simp: rtrancl_is_UN_relpow)
- apply (rule_tac x="Suc n" in exI)
+ apply (rule_tac x="Suc x" in exI)
apply (clarsimp simp: relcomp_unfold)
apply fastforce
apply clarsimp
@@ -1093,9 +1093,9 @@
assumes "finite R" and "finite S"
shows "finite(R O S)"
proof-
- have "R O S = (UN (x,y) : R. \<Union>((%(u,v). if u=y then {(x,v)} else {}) ` S))"
- by(force simp add: split_def)
- thus ?thesis using assms by(clarsimp)
+ have "R O S = (\<Union>(x, y)\<in>R. \<Union>(u, v)\<in>S. if u = y then {(x, v)} else {})"
+ by (force simp add: split_def image_constant_conv split: if_splits)
+ then show ?thesis using assms by clarsimp
qed
lemma finite_relpow[simp,intro]: