diff -r 1e7f2d296e19 -r 46e441e61ff5 src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Sun Dec 15 15:10:14 2013 +0100
+++ b/src/HOL/Groups_Big.thy	Sun Dec 15 15:10:16 2013 +0100
@@ -20,8 +20,8 @@
 interpretation comp_fun_commute f
   by default (simp add: fun_eq_iff left_commute)
 
-interpretation comp_fun_commute "f \<circ> g"
-  by (rule comp_comp_fun_commute)
+interpretation comp?: comp_fun_commute "f \<circ> g"
+  by (fact comp_comp_fun_commute)
 
 definition F :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a"
 where