From 98cace9bf83768f001c635b418f4dfc430831718 Mon Sep 17 00:00:00 2001
From: Jeremy Avigad <avigad@cmu.edu>
Date: Sat, 11 Jul 2015 14:43:18 +1000
Subject: [PATCH] fix(library/data/finset/bigops): remove extraneous parameter

---
 library/data/finset/bigops.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/library/data/finset/bigops.lean b/library/data/finset/bigops.lean
index 62185d3f41..ac69062389 100644
--- a/library/data/finset/bigops.lean
+++ b/library/data/finset/bigops.lean
@@ -118,8 +118,8 @@ section deceqA
         (by rewrite Union_empty)
         (take s1 a Pa IH, by rewrite [image_insert, *Union_insert, IH])
 
-  lemma Union_const [deceqB : decidable_eq B] {f : A → finset B} {s : finset A} {t : finset B}
-    (a : A) : s ≠ ∅ → (∀ x, x ∈ s → f x = t) → Union s f = t :=
+  lemma Union_const [deceqB : decidable_eq B] {f : A → finset B} {s : finset A} {t : finset B} :
+    s ≠ ∅ → (∀ x, x ∈ s → f x = t) → Union s f = t :=
   begin
     induction s with a' s' H IH,
       {intros [H1, H2], exfalso, apply H1 !rfl},