src/HOL/Finite_Set.thy

 lemma (in ACe) fold_Un_Int:
   "finite A ==> finite B ==>
     fold f e A \<cdot> fold f e B = fold f e (A Un B) \<cdot> fold f e (A Int B)"
   apply (induct set: Finites)
    apply simp
-  apply (simp add: AC ACe_axioms ACe_axioms_def
-    LC_axioms_def LC.fold_insert insert_absorb Int_insert_left)
+  apply (simp add: AC insert_absorb Int_insert_left
+    LC.fold_insert [OF LC.intro, OF LC_axioms.intro])
   done
 
 lemma (in ACe) fold_Un_disjoint:
   "finite A ==> finite B ==> A Int B = {} ==>
     fold f e (A Un B) = fold f e A \<cdot> fold f e B"

   next
     case (insert F x)
     have "fold (f \<circ> g) e (insert x F \<union> B) = fold (f \<circ> g) e (insert x (F \<union> B))"
       by simp
     also have "... = (f \<circ> g) x (fold (f \<circ> g) e (F \<union> B))"
-      by (rule LC.fold_insert)
+      by (rule LC.fold_insert [OF LC.intro])
         (insert b insert, auto simp add: left_commute intro: LC_axioms.intro)
     also from insert have "fold (f \<circ> g) e (F \<union> B) =
       fold (f \<circ> g) e F \<cdot> fold (f \<circ> g) e B" by blast
     also have "(f \<circ> g) x ... = (f \<circ> g) x (fold (f \<circ> g) e F) \<cdot> fold (f \<circ> g) e B"
       by (simp add: AC)
     also have "(f \<circ> g) x (fold (f \<circ> g) e F) = fold (f \<circ> g) e (insert x F)"
-      by (rule LC.fold_insert [symmetric]) (insert b insert,
+      by (rule LC.fold_insert [OF LC.intro, symmetric]) (insert b insert,
 	auto simp add: left_commute intro: LC_axioms.intro)
     finally show ?case .
   qed
 qed
 

   by (simp add: setsum_def)
 
 lemma setsum_insert [simp]:
     "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
   by (simp add: setsum_def
-    LC_axioms_def LC.fold_insert plus_ac0_left_commute)
+    LC.fold_insert [OF LC.intro, OF LC_axioms.intro] plus_ac0_left_commute)
 
 lemma setsum_0: "setsum (\<lambda>i. 0) A = 0"
   apply (case_tac "finite A")
    prefer 2 apply (simp add: setsum_def)
   apply (erule finite_induct)