# HG changeset patch
# User wenzelm
# Date 1027097076 -7200
# Node ID dbb608cd11c4ea0bdf4a694e60c5eada5329d9c7
# Parent  c136276dc8479b77b7aff25c910ce141b7095c3a
accomodate cumulative locale predicates;

diff -r c136276dc847 -r dbb608cd11c4 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Fri Jul 19 18:44:07 2002 +0200
+++ b/src/HOL/Finite_Set.thy	Fri Jul 19 18:44:36 2002 +0200
@@ -720,8 +720,8 @@
     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:
@@ -745,14 +745,14 @@
     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
@@ -779,7 +779,7 @@
 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")