src/HOL/Finite_Set.thy

   A Tutorial on the Universality and Expressiveness of Fold,
   JFP 9:4 (355-372), 1999.
 *}
 
 lemma fold_fusion:
-  includes ab_semigroup_mult g
+  assumes "ab_semigroup_mult g"
   assumes fin: "finite A"
     and hyp: "\<And>x y. h (g x y) = times x (h y)"
   shows "h (fold g j w A) = fold times j (h w) A"
-  using fin hyp by (induct set: finite) simp_all
+proof -
+  interpret ab_semigroup_mult [g] by fact
+  show ?thesis using fin hyp by (induct set: finite) simp_all
+qed
 
 lemma fold_cong:
   "finite A \<Longrightarrow> (!!x. x:A ==> g x = h x) ==> fold times g z A = fold times h z A"
   apply (subgoal_tac "ALL C. C <= A --> (ALL x:C. g x = h x) --> fold times g z C = fold times h z C")
    apply simp