1.1 --- a/src/HOL/Finite_Set.thy	Thu Sep 19 16:09:16 2002 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Fri Sep 20 11:48:35 2002 +0200
     1.3 @@ -744,16 +744,16 @@
     1.4      thus ?case by simp
     1.5    next
     1.6      case (insert F x)
     1.7 -    have "fold (f \<circ> g) e (insert x F \<union> B) = fold (f \<circ> g) e (insert x (F \<union> B))"
     1.8 +    have "fold (f o g) e (insert x F \<union> B) = fold (f o g) e (insert x (F \<union> B))"
     1.9        by simp
    1.10 -    also have "... = (f \<circ> g) x (fold (f \<circ> g) e (F \<union> B))"
    1.11 +    also have "... = (f o g) x (fold (f o g) e (F \<union> B))"
    1.12        by (rule LC.fold_insert [OF LC.intro])
    1.13          (insert b insert, auto simp add: left_commute)
    1.14 -    also from insert have "fold (f \<circ> g) e (F \<union> B) =
    1.15 -      fold (f \<circ> g) e F \<cdot> fold (f \<circ> g) e B" by blast
    1.16 -    also have "(f \<circ> g) x ... = (f \<circ> g) x (fold (f \<circ> g) e F) \<cdot> fold (f \<circ> g) e B"
    1.17 +    also from insert have "fold (f o g) e (F \<union> B) =
    1.18 +      fold (f o g) e F \<cdot> fold (f o g) e B" by blast
    1.19 +    also have "(f o g) x ... = (f o g) x (fold (f o g) e F) \<cdot> fold (f o g) e B"
    1.20        by (simp add: AC)
    1.21 -    also have "(f \<circ> g) x (fold (f \<circ> g) e F) = fold (f \<circ> g) e (insert x F)"
    1.22 +    also have "(f o g) x (fold (f o g) e F) = fold (f o g) e (insert x F)"
    1.23        by (rule LC.fold_insert [OF LC.intro, symmetric]) (insert b insert,
    1.24  	auto simp add: left_commute)
    1.25      finally show ?case .