src/HOL/Hilbert_Choice.thy

--- a/src/HOL/Hilbert_Choice.thy	Mon Oct 08 11:37:03 2012 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Mon Oct 08 12:03:49 2012 +0200
@@ -144,7 +144,7 @@
 by (simp add: inj_iff)
 
 lemma o_inv_o_cancel[simp]: "inj f ==> g o inv f o f = g"
-by (simp add: o_assoc[symmetric])
+by (simp add: comp_assoc)
 
 lemma inv_into_image_cancel[simp]:
   "inj_on f A ==> S <= A ==> inv_into A f ` f ` S = S"