diff -r bb3986d95562 -r a9c40cf517d1 src/HOL/Transitive_Closure.thy
--- 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: