--- a/src/HOL/List.thy Wed Aug 22 12:32:57 2018 +0000
+++ b/src/HOL/List.thy Wed Aug 22 12:32:58 2018 +0000
@@ -2983,11 +2983,11 @@
lemma (in complete_lattice) INF_set_fold:
"INFIMUM (set xs) f = fold (inf \<circ> f) xs top"
- using Inf_set_fold [of "map f xs "] by (simp add: fold_map)
+ using Inf_set_fold [of "map f xs"] by (simp add: fold_map)
lemma (in complete_lattice) SUP_set_fold:
"SUPREMUM (set xs) f = fold (sup \<circ> f) xs bot"
- using Sup_set_fold [of "map f xs "] by (simp add: fold_map)
+ using Sup_set_fold [of "map f xs"] by (simp add: fold_map)
subsubsection \<open>Fold variants: @{const foldr} and @{const foldl}\<close>