# HG changeset patch
# User haftmann
# Date 1388249514 -3600
# Node ID 1b5f2485757bf5824edf370b8a7c5cc4028e9641
# Parent  0046711700c8b5b44600bdc41535d8f2cc447cd3
prefix disambiguation

diff -r 0046711700c8 -r 1b5f2485757b src/HOL/Finite_Set.thy
--- 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]: