fix more looping simp rules

--- a/src/HOL/Library/Formal_Power_Series.thy	Wed Feb 17 10:00:22 2010 -0800
+++ b/src/HOL/Library/Formal_Power_Series.thy	Wed Feb 17 10:30:36 2010 -0800
@@ -2864,8 +2864,8 @@
     then have nz: "pochhammer (1 + b - of_nat n) n \<noteq> 0" 
       by (auto simp add: algebra_simps)
     
-    from nz kn have nz': "pochhammer (1 + b - of_nat n) k \<noteq> 0" 
-      by (simp add: pochhammer_neq_0_mono)
+    from nz kn [simplified] have nz': "pochhammer (1 + b - of_nat n) k \<noteq> 0" 
+      by (rule pochhammer_neq_0_mono)
     {assume k0: "k = 0 \<or> n =0" 
       then have "b gchoose (n - k) = (?m1 n * ?p b n * ?m1 k * ?p (of_nat n) k) / (?f n * pochhammer (b - of_nat n + 1) k)" 
         using kn

--- a/src/HOL/Library/Ramsey.thy	Wed Feb 17 10:00:22 2010 -0800
+++ b/src/HOL/Library/Ramsey.thy	Wed Feb 17 10:30:36 2010 -0800
@@ -111,7 +111,7 @@
         have infYx': "infinite (Yx-{yx'})" using fields px by auto
         with fields px yx' Suc.prems
         have partfx': "part r s (Yx - {yx'}) (f \<circ> insert yx')"
-          by (simp add: o_def part_Suc_imp_part part_subset [where ?YY=YY]) 
+          by (simp add: o_def part_Suc_imp_part part_subset [where YY=YY and Y=Yx])
         from Suc.hyps [OF infYx' partfx']
         obtain Y' and t'
         where Y': "Y' \<subseteq> Yx - {yx'}"  "infinite Y'"  "t' < s"

--- a/src/HOL/Library/Word.thy	Wed Feb 17 10:00:22 2010 -0800
+++ b/src/HOL/Library/Word.thy	Wed Feb 17 10:30:36 2010 -0800
@@ -980,7 +980,8 @@
   fix xs
   assume "length (norm_signed (\<zero>#xs)) = Suc (length xs)"
   thus "norm_signed (\<zero>#xs) = \<zero>#xs"
-    by (simp add: norm_signed_Cons norm_unsigned_equal split: split_if_asm)
+    by (simp add: norm_signed_Cons norm_unsigned_equal [THEN eqTrueI]
+             split: split_if_asm)
 next
   fix xs
   assume "length (norm_signed (\<one>#xs)) = Suc (length xs)"

--- a/src/HOL/Library/Zorn.thy	Wed Feb 17 10:00:22 2010 -0800
+++ b/src/HOL/Library/Zorn.thy	Wed Feb 17 10:30:36 2010 -0800
@@ -333,7 +333,7 @@
 
 lemma antisym_init_seg_of:
   "r initial_segment_of s \<Longrightarrow> s initial_segment_of r \<Longrightarrow> r=s"
-by(auto simp:init_seg_of_def)
+unfolding init_seg_of_def by safe
 
 lemma Chain_init_seg_of_Union:
   "R \<in> Chain init_seg_of \<Longrightarrow> r\<in>R \<Longrightarrow> r initial_segment_of \<Union>R"