diff -r 162bd20dae23 -r b57df8eecad6 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/Transitive_Closure.thy	Thu Aug 27 21:19:48 2015 +0200
@@ -169,8 +169,9 @@
 
 lemma rtrancl_Int_subset: "[| Id \<subseteq> s; (r^* \<inter> s) O r \<subseteq> s|] ==> r^* \<subseteq> s"
   apply (rule subsetI)
-  apply (rule_tac p="x" in PairE, clarify)
-  apply (erule rtrancl_induct, auto) 
+  apply auto
+  apply (erule rtrancl_induct)
+  apply auto
   done
 
 lemma converse_rtranclp_into_rtranclp:
@@ -409,10 +410,9 @@
 
 lemma trancl_Int_subset: "[| r \<subseteq> s; (r^+ \<inter> s) O r \<subseteq> s|] ==> r^+ \<subseteq> s"
   apply (rule subsetI)
-  apply (rule_tac p = x in PairE)
-  apply clarify
+  apply auto
   apply (erule trancl_induct)
-   apply auto
+  apply auto
   done
 
 lemma trancl_unfold: "r^+ = r Un r^+ O r"