# HG changeset patch
# User haftmann
# Date 1325162541 -3600
# Node ID 773c0c4994dfcb1b8cb00c4773ee3f011be56bee
# Parent  6fc579c917b8d91ada6fb71bc8643e363476b7df
qualified Finite_Set.fold

diff -r 6fc579c917b8 -r 773c0c4994df src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Dec 29 13:41:41 2011 +0100
+++ b/src/HOL/List.thy	Thu Dec 29 13:42:21 2011 +0100
@@ -2511,11 +2511,11 @@
 text {* @{const Finite_Set.fold} and @{const foldl} *}
 
 lemma (in comp_fun_commute) fold_set_remdups:
-  "fold f y (set xs) = foldl (\<lambda>y x. f x y) y (remdups xs)"
+  "Finite_Set.fold f y (set xs) = foldl (\<lambda>y x. f x y) y (remdups xs)"
   by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm insert_absorb)
 
 lemma (in comp_fun_idem) fold_set:
-  "fold f y (set xs) = foldl (\<lambda>y x. f x y) y xs"
+  "Finite_Set.fold f y (set xs) = foldl (\<lambda>y x. f x y) y xs"
   by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm)
 
 lemma (in ab_semigroup_idem_mult) fold1_set:
@@ -2530,7 +2530,7 @@
     case True with xs show ?thesis by simp
   next
     case False
-    then have "fold1 times (insert y (set ys)) = fold times y (set ys)"
+    then have "fold1 times (insert y (set ys)) = Finite_Set.fold times y (set ys)"
       by (simp only: finite_set fold1_eq_fold_idem)
     with xs show ?thesis by (simp add: fold_set mult_commute)
   qed