src/HOL/Finite_Set.thy

--- a/src/HOL/Finite_Set.thy	Mon May 09 16:11:20 2011 +0200
+++ b/src/HOL/Finite_Set.thy	Thu May 12 11:03:48 2011 +0200
@@ -539,7 +539,7 @@
 
 text{* On a functional level it looks much nicer: *}
 
-lemma fun_comp_comm:  "f x \<circ> f y = f y \<circ> f x"
+lemma commute_comp: "f y \<circ> f x = f x \<circ> f y"
 by (simp add: fun_left_comm fun_eq_iff)
 
 end