src/HOL/Finite_Set.thy

   fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
   fixes z :: "'b"
   assumes comp_fun_commute: "f y \<circ> f x = f x \<circ> f y"
 begin
 
-interpretation comp_fun_commute f
+interpretation fold?: comp_fun_commute f
   by default (insert comp_fun_commute, simp add: fun_eq_iff)
 
 definition F :: "'a set \<Rightarrow> 'b"
 where
   eq_fold: "F A = fold f z A"

   assumes comp_fun_idem: "f x \<circ> f x = f x"
 begin
 
 declare insert [simp del]
 
-interpretation comp_fun_idem f
+interpretation fold?: comp_fun_idem f
   by default (insert comp_fun_commute comp_fun_idem, simp add: fun_eq_iff)
 
 lemma insert_idem [simp]:
   assumes "finite A"
   shows "F (insert x A) = f x (F A)"