
diff -r 1e1611fd32df -r 13aa6d8268ec src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Mon Oct 08 11:37:03 2012 +0200
+++ b/src/HOL/Finite_Set.thy	Mon Oct 08 12:03:49 2012 +0200
@@ -793,7 +793,7 @@
         with Suc have hyp: "f y ^^ h y \<circ> f x = f x \<circ> f y ^^ h y"
           by auto
         from Suc h_def have "g y = Suc (h y)" by simp
-        then show ?case by (simp add: o_assoc [symmetric] hyp)
+        then show ?case by (simp add: comp_assoc hyp)
           (simp add: o_assoc comp_fun_commute)
       qed
       def h \<equiv> "\<lambda>z. if z = x then g x - 1 else g z"
@@ -803,7 +803,7 @@
       with False h_def have hyp2: "f y ^^ g y \<circ> f x ^^ h x = f x ^^ h x \<circ> f y ^^ g y" by simp
       from Suc h_def have "g x = Suc (h x)" by simp
       then show ?case by (simp del: funpow.simps add: funpow_Suc_right o_assoc hyp2)
-        (simp add: o_assoc [symmetric] hyp1)
+        (simp add: comp_assoc hyp1)
     qed
   qed
 qed
@@ -1507,7 +1507,7 @@
   assumes "finite A"
   shows "f x \<circ> F A = F A \<circ> f x"
   using assms by (induct A)
-    (simp, simp del: o_apply add: o_assoc, simp del: o_apply add: o_assoc [symmetric] comp_fun_commute)
+    (simp, simp del: o_apply add: o_assoc, simp del: o_apply add: comp_assoc comp_fun_commute)
 
 lemma commute_left_comp':
   assumes "finite A"
@@ -1518,14 +1518,14 @@
   assumes "finite A" and "finite B"
   shows "F B \<circ> F A = F A \<circ> F B"
   using assms by (induct A)
-    (simp_all add: o_assoc, simp add: o_assoc [symmetric] comp_fun_commute')
+    (simp_all add: o_assoc, simp add: comp_assoc comp_fun_commute')
 
 lemma commute_left_comp'':
   assumes "finite A" and "finite B"
   shows "F B \<circ> (F A \<circ> g) = F A \<circ> (F B \<circ> g)"
   using assms by (simp add: o_assoc comp_fun_commute'')
 
-lemmas comp_fun_commutes = o_assoc [symmetric] comp_fun_commute commute_left_comp
+lemmas comp_fun_commutes = comp_assoc comp_fun_commute commute_left_comp
   comp_fun_commute' commute_left_comp' comp_fun_commute'' commute_left_comp''
 
 lemma union_inter:




