--- a/src/HOL/Finite_Set.thy Fri Dec 27 20:35:32 2013 +0100
+++ b/src/HOL/Finite_Set.thy Sat Dec 28 17:51:54 2013 +0100
@@ -1085,7 +1085,7 @@
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"
@@ -1135,7 +1135,7 @@
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]: