odd workaround for odd problem of load order in HOL/ex/ROOT.ML (!??);
authorwenzelm
Sat, 20 Aug 2011 23:36:18 +0200
changeset 44339 eda6aef75939
parent 44338 700008399ee5
child 44340 3b859b573f1a
odd workaround for odd problem of load order in HOL/ex/ROOT.ML (!??);
src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sat Aug 20 23:35:30 2011 +0200
+++ b/src/HOL/Library/Multiset.thy	Sat Aug 20 23:36:18 2011 +0200
@@ -1598,7 +1598,7 @@
 definition image_mset :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a multiset \<Rightarrow> 'b multiset" where
   "image_mset f = fold_mset (op + o single o f) {#}"
 
-interpretation image_fun_commute: comp_fun_commute "op + o single o f"
+interpretation image_fun_commute: comp_fun_commute "op + o single o f" for f
 proof qed (simp add: add_ac fun_eq_iff)
 
 lemma image_mset_empty [simp]: "image_mset f {#} = {#}"