# HG changeset patch
# User haftmann
# Date 1534941178 0
# Node ID 567079abb17354d430ceab04dcc4554ffc5dc096
# Parent  54fdc8bc73a3b1adff0be1f20535a085981e3cc4
tuned whitespace

diff -r 54fdc8bc73a3 -r 567079abb173 src/HOL/List.thy
--- 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>