--- a/src/HOL/Transitive_Closure.thy Mon Apr 11 15:50:50 2016 +0200
+++ b/src/HOL/Transitive_Closure.thy Tue Apr 12 13:49:37 2016 +0200
@@ -534,7 +534,7 @@
lemma irrefl_tranclI: "r^-1 \<inter> r^* = {} ==> (x, x) \<notin> r^+"
by (blast elim: tranclE dest: trancl_into_rtrancl)
-lemma irrefl_trancl_rD: "!!X. ALL x. (x, x) \<notin> r^+ ==> (x, y) \<in> r ==> x \<noteq> y"
+lemma irrefl_trancl_rD: "\<forall>x. (x, x) \<notin> r^+ \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> x \<noteq> y"
by (blast dest: r_into_trancl)
lemma trancl_subset_Sigma_aux: