r_into_(r)trancl should not be [simp]: helps little and comlicates some AFP proofs

--- a/src/HOL/Transitive_Closure.thy	Sat Jun 21 15:46:52 2014 +0200
+++ b/src/HOL/Transitive_Closure.thy	Sun Jun 22 12:37:55 2014 +0200
@@ -87,7 +87,7 @@
 lemma reflcl_set_eq [pred_set_conv]: "(sup (\<lambda>x y. (x, y) \<in> r) op =) = (\<lambda>x y. (x, y) \<in> r \<union> Id)"
   by (auto simp add: fun_eq_iff)
 
-lemma r_into_rtrancl [intro,simp]: "!!p. p \<in> r ==> p \<in> r^*"
+lemma r_into_rtrancl [intro]: "!!p. p \<in> r ==> p \<in> r^*"
   -- {* @{text rtrancl} of @{text r} contains @{text r} *}
   apply (simp only: split_tupled_all)
   apply (erule rtrancl_refl [THEN rtrancl_into_rtrancl])
@@ -340,7 +340,7 @@
    apply (iprover dest: subsetD)+
   done
 
-lemma r_into_trancl'[simp]: "!!p. p : r ==> p : r^+"
+lemma r_into_trancl': "!!p. p : r ==> p : r^+"
   by (simp only: split_tupled_all) (erule r_into_trancl)
 
 text {*

--- a/src/HOL/UNITY/Comp/PriorityAux.thy	Sat Jun 21 15:46:52 2014 +0200
+++ b/src/HOL/UNITY/Comp/PriorityAux.thy	Sun Jun 22 12:37:55 2014 +0200
@@ -95,7 +95,7 @@
 apply (erule ImageE)
 apply (erule trancl_induct) 
  apply (cases "i=k", simp_all) 
- apply (blast, clarify) 
+ apply (blast, blast, clarify) 
 apply (drule_tac x = y in spec)
 apply (drule_tac x = z in spec)
 apply (blast dest: r_into_trancl intro: trancl_trans)