diff --git a/library/init/control/except.lean b/library/init/control/except.lean
index de4eadae62..717ac1f552 100644
--- a/library/init/control/except.lean
+++ b/library/init/control/except.lean
@@ -50,7 +50,6 @@ section
   match ma with
   | (except.error err) := except.error err
   | (except.ok v) := f v
-  end
 
   protected def to_bool {α : Type v} : except ε α → bool
   | (except.ok _)    := tt
@@ -94,8 +93,7 @@ section
   protected def catch {α : Type u} (ma : except_t ε m α) (handle : ε → except_t ε m α) : except_t ε m α :=
   ⟨ma.run >>= λ res, match res with
    | except.ok a    := pure (except.ok a)
-   | except.error e := (handle e).run
-   end⟩
+   | except.error e := (handle e).run⟩
 
   @[inline] protected def monad_map {m'} [monad m'] {α} (f : ∀ {α}, m α → m' α) : except_t ε m α → except_t ε m' α :=
   λ x, ⟨f x.run⟩
diff --git a/library/init/data/bool/lemmas.lean b/library/init/data/bool/lemmas.lean
index 230c237dd3..232495be79 100644
--- a/library/init/data/bool/lemmas.lean
+++ b/library/init/data/bool/lemmas.lean
@@ -111,7 +111,6 @@ show (tt = tt) = true, by simp
 match d with
 | is_true hp := ⟨λh, hp, λ_, rfl⟩
 | is_false hnp := ⟨λh, bool.no_confusion h, λhp, absurd hp hnp⟩
-end
 
 theorem to_bool_true {p : Prop} [decidable p] : p → to_bool p := (to_bool_iff p).2
 
diff --git a/library/init/data/hashmap/basic.lean b/library/init/data/hashmap/basic.lean
index 141e5a40ed..def4e32357 100644
--- a/library/init/data/hashmap/basic.lean
+++ b/library/init/data/hashmap/basic.lean
@@ -114,17 +114,14 @@ variables {α : Type u} {β : α → Type v} [decidable_eq α] {h : α → usize
 def insert (m : d_hashmap α β h) (a : α) (b : β a) : d_hashmap α β h :=
 match m with
 | ⟨ m, hw ⟩ := ⟨ m.insert h a b, well_formed.insert_wff m a b hw ⟩
-end
 
 def erase (m : d_hashmap α β h) (a : α) : d_hashmap α β h :=
 match m with
 | ⟨ m, hw ⟩ := ⟨ m.erase h a, well_formed.erase_wff m a hw ⟩
-end
 
 def find (m : d_hashmap α β h) (a : α) : option (β a) :=
 match m with
 | ⟨ m, _ ⟩ := m.find h a
-end
 
 @[inline] def contains (m : d_hashmap α β h) (a : α) : bool :=
 (m.find a).is_some
@@ -132,12 +129,10 @@ end
 def fold {δ : Type w} (m : d_hashmap α β h) (d : δ) (f : δ → Π a, β a → δ) : δ :=
 match m with
 | ⟨ m, _ ⟩ := m.fold d f
-end
 
 def size (m : d_hashmap α β h) : nat :=
 match m with
 | ⟨ {size := sz, ..}, _ ⟩ := sz
-end
 
 @[inline] def empty (m : d_hashmap α β h) : bool :=
 m.size = 0
diff --git a/library/init/data/int/basic.lean b/library/init/data/int/basic.lean
index dccfba6555..8d29b281a3 100644
--- a/library/init/data/int/basic.lean
+++ b/library/init/data/int/basic.lean
@@ -57,7 +57,6 @@ def sub_nat_nat (m n : ℕ) : int :=
 match (n - m : nat) with
 | 0        := of_nat (m - n)  -- m ≥ n
 | (succ k) := -[1+ k]         -- m < n, and n - m = succ k
-end
 
 protected def neg : int → int
 | (of_nat n) := neg_of_nat n
diff --git a/library/init/data/list/basic.lean b/library/init/data/list/basic.lean
index 883065f990..bea78899e5 100644
--- a/library/init/data/list/basic.lean
+++ b/library/init/data/list/basic.lean
@@ -23,12 +23,10 @@ protected def has_dec_eq [s : decidable_eq α] : decidable_eq (list α)
 | (a::as) (b::bs) :=
   match s a b with
   | is_true hab  :=
-    match has_dec_eq as bs with
-    | is_true habs  := is_true (eq.subst hab (eq.subst habs rfl))
-    | is_false nabs := is_false (λ h, list.no_confusion h (λ _ habs, absurd habs nabs))
-    end
+    (match has_dec_eq as bs with
+     | is_true habs  := is_true (eq.subst hab (eq.subst habs rfl))
+     | is_false nabs := is_false (λ h, list.no_confusion h (λ _ habs, absurd habs nabs)))
   | is_false nab := is_false (λ h, list.no_confusion h (λ hab _, absurd hab nab))
-  end
 
 instance [decidable_eq α] : decidable_eq (list α) :=
 list.has_dec_eq
@@ -61,9 +59,8 @@ instance decidable_mem [decidable_eq α] (a : α) : ∀ (l : list α), decidable
 | (b::l) :=
   if h₁ : a = b then is_true (or.inl h₁)
   else match decidable_mem l with
-  | is_true  h₂ := is_true (or.inr h₂)
-  | is_false h₂ := is_false (not_or h₁ h₂)
-  end
+       | is_true  h₂ := is_true (or.inr h₂)
+       | is_false h₂ := is_false (not_or h₁ h₂)
 
 instance : has_emptyc (list α) :=
 ⟨list.nil⟩
@@ -135,7 +132,6 @@ def filter_map (f : α → option β) : list α → list β
   match f a with
   | none   := filter_map l
   | some b := b :: filter_map l
-  end
 
 def filter (p : α → Prop) [decidable_pred p] : list α → list α
 | []     := []
@@ -209,7 +205,7 @@ zip_with prod.mk
 
 def unzip : list (α × β) → list α × list β
 | []            := ([], [])
-| ((a, b) :: t) := match unzip t with (al, bl) := (a::al, b::bl) end
+| ((a, b) :: t) := match unzip t with | (al, bl) := (a::al, b::bl)
 
 protected def insert [decidable_eq α] (a : α) (l : list α) : list α :=
 if a ∈ l then l else a :: l
@@ -300,8 +296,6 @@ instance has_decidable_lt [has_lt α] [h : decidable_rel ((<) : α → α → Pr
     match has_decidable_lt as bs with
     | is_true h₂  := is_true (or.inr h₂)
     | is_false h₂ := is_false (λ hd, or.elim hd (λ n₁, absurd n₁ h₁) (λ n₂, absurd n₂ h₂))
-    end
-  end
 
 @[reducible] protected def le [has_lt α] (a b : list α) : Prop :=
 ¬ b < a
diff --git a/library/init/data/option/basic.lean b/library/init/data/option/basic.lean
index 508de3f31d..1935e7474a 100644
--- a/library/init/data/option/basic.lean
+++ b/library/init/data/option/basic.lean
@@ -43,7 +43,7 @@ protected def map {α β} (f : α → β) (o : option α) : option β :=
 option.bind o (some ∘ f)
 
 theorem map_id {α} : (option.map id : option α → option α) = id :=
-funext (λo, match o with | none := rfl | some x := rfl end)
+funext (λo, match o with | none := rfl | some x := rfl)
 
 instance : monad option :=
 {pure := @some, bind := @option.bind, map := @option.map}
@@ -81,6 +81,5 @@ instance {α : Type u} [d : decidable_eq α] : decidable_eq (option α)
   match (d v₁ v₂) with
   | (is_true e)  := is_true (congr_arg (@some α) e)
   | (is_false n) := is_false (λ h, option.no_confusion h (λ e, absurd e n))
-  end
 
 instance {α : Type u} [has_lt α] : has_lt (option α) := ⟨option.lt (<)⟩
diff --git a/library/init/data/ordering/basic.lean b/library/init/data/ordering/basic.lean
index 2d48d62aca..3f8de2d4b2 100644
--- a/library/init/data/ordering/basic.lean
+++ b/library/init/data/ordering/basic.lean
@@ -12,7 +12,7 @@ inductive ordering
 | lt | eq | gt
 
 instance : has_repr ordering :=
-⟨(λ s, match s with | ordering.lt := "lt" | ordering.eq := "eq" | ordering.gt := "gt" end)⟩
+⟨(λ s, match s with | ordering.lt := "lt" | ordering.eq := "eq" | ordering.gt := "gt")⟩
 
 namespace ordering
 def swap : ordering → ordering
@@ -43,21 +43,17 @@ instance : decidable_eq ordering :=
 λ a b,
   match a with
   | ordering.lt :=
-    match b with
-    | ordering.lt := is_true rfl
-    | ordering.eq := is_false (λ h, ordering.no_confusion h)
-    | ordering.gt := is_false (λ h, ordering.no_confusion h)
-    end
+    (match b with
+     | ordering.lt := is_true rfl
+     | ordering.eq := is_false (λ h, ordering.no_confusion h)
+     | ordering.gt := is_false (λ h, ordering.no_confusion h))
   | ordering.eq :=
-    match b with
-    | ordering.lt := is_false (λ h, ordering.no_confusion h)
-    | ordering.eq := is_true rfl
-    | ordering.gt := is_false (λ h, ordering.no_confusion h)
-    end
+    (match b with
+     | ordering.lt := is_false (λ h, ordering.no_confusion h)
+     | ordering.eq := is_true rfl
+     | ordering.gt := is_false (λ h, ordering.no_confusion h))
   | ordering.gt :=
     match b with
     | ordering.lt := is_false (λ h, ordering.no_confusion h)
     | ordering.eq := is_false (λ h, ordering.no_confusion h)
     | ordering.gt := is_true rfl
-    end
-  end
diff --git a/library/init/data/rbmap/basic.lean b/library/init/data/rbmap/basic.lean
index f8a8debf70..c514db86bb 100644
--- a/library/init/data/rbmap/basic.lean
+++ b/library/init/data/rbmap/basic.lean
@@ -50,7 +50,6 @@ match m.val with
 | rbnode.leaf             := false
 | rbnode.red_node _ e _   := rbtree.mem (k, e.2) m
 | rbnode.black_node _ e _ := rbtree.mem (k, e.2) m
-end
 
 instance : has_mem α (rbmap α β lt) :=
 ⟨rbmap.mem⟩
@@ -71,7 +70,6 @@ match m.val with
 | rbnode.leaf             := none
 | rbnode.red_node _ e _   := @rbtree.find _ _ rbmap_lt_dec m (k, e.2)
 | rbnode.black_node _ e _ := @rbtree.find _ _ rbmap_lt_dec m (k, e.2)
-end
 
 def to_value : option (α × β) → option β
 | none     := none
diff --git a/library/init/data/rbtree/basic.lean b/library/init/data/rbtree/basic.lean
index c10c178154..47e1d99153 100644
--- a/library/init/data/rbtree/basic.lean
+++ b/library/init/data/rbtree/basic.lean
@@ -96,11 +96,10 @@ variables (lt : α → α → Prop) [decidable_rel lt]
 def ins : rbnode α → α → rbnode α
 | leaf             x  := red_node leaf x leaf
 | (red_node a y b) x  :=
-   match cmp_using lt x y with
-   | ordering.lt := red_node (ins a x) y b
-   | ordering.eq := red_node a x b
-   | ordering.gt := red_node a y (ins b x)
-   end
+   (match cmp_using lt x y with
+    | ordering.lt := red_node (ins a x) y b
+    | ordering.eq := red_node a x b
+    | ordering.gt := red_node a y (ins b x))
 | (black_node a y b) x :=
     match cmp_using lt x y with
     | ordering.lt :=
@@ -110,7 +109,6 @@ def ins : rbnode α → α → rbnode α
     | ordering.gt :=
       if b.get_color = red then balance2_node (ins b x) y a
       else black_node a y (ins b x)
-    end
 
 def mk_insert_result : color → rbnode α → rbnode α
 | red (red_node l v r)   := black_node l v r
@@ -140,17 +138,15 @@ variable [decidable_rel lt]
 def find : rbnode α → α → option α
 | leaf             x := none
 | (red_node a y b) x :=
-  match cmp_using lt x y with
-  | ordering.lt := find a x
-  | ordering.eq := some y
-  | ordering.gt := find b x
-  end
+  (match cmp_using lt x y with
+   | ordering.lt := find a x
+   | ordering.eq := some y
+   | ordering.gt := find b x)
 | (black_node a y b) x :=
-  match cmp_using lt x y with
-  | ordering.lt := find a x
-  | ordering.eq := some y
-  | ordering.gt := find b x
-  end
+  (match cmp_using lt x y with
+   | ordering.lt := find a x
+   | ordering.eq := some y
+   | ordering.gt := find b x)
 
 end membership
 
diff --git a/library/init/data/repr.lean b/library/init/data/repr.lean
index 147a0b56a0..ef94099cab 100644
--- a/library/init/data/repr.lean
+++ b/library/init/data/repr.lean
@@ -38,10 +38,10 @@ instance : has_repr unit :=
 ⟨λ u, "()"⟩
 
 instance {α : Type u} [has_repr α] : has_repr (option α) :=
-⟨λ o, match o with | none := "none" | (some a) := "(some " ++ repr a ++ ")" end⟩
+⟨λ o, match o with | none := "none" | (some a) := "(some " ++ repr a ++ ")"⟩
 
 instance {α : Type u} {β : Type v} [has_repr α] [has_repr β] : has_repr (α ⊕ β) :=
-⟨λ s, match s with | (inl a) := "(inl " ++ repr a ++ ")" | (inr b) := "(inr " ++ repr b ++ ")" end⟩
+⟨λ s, match s with | (inl a) := "(inl " ++ repr a ++ ")" | (inr b) := "(inr " ++ repr b ++ ")"⟩
 
 instance {α : Type u} {β : Type v} [has_repr α] [has_repr β] : has_repr (α × β) :=
 ⟨λ ⟨a, b⟩, "(" ++ repr a ++ ", " ++ repr b ++ ")"⟩
diff --git a/library/init/data/string/basic.lean b/library/init/data/string/basic.lean
index 0ca3ee5103..313676320f 100644
--- a/library/init/data/string/basic.lean
+++ b/library/init/data/string/basic.lean
@@ -126,16 +126,14 @@ protected def extract_core : list char → list char → option (list char)
   match extract_core cs₁ cs₂ with
   | none   := none
   | some r := some (c::r)
-  end
 
 def extract : iterator → iterator → option string
 | ⟨p₁, n₁⟩ ⟨p₂, n₂⟩ :=
   if p₁.reverse ++ n₁ ≠ p₂.reverse ++ n₂ then none
   else if n₁ = n₂ then some ""
-  else match iterator.extract_core n₁ n₂ with
-       | none := none
-       | some r := some ⟨r⟩
-       end
+  else (match iterator.extract_core n₁ n₂ with
+        | none := none
+        | some r := some ⟨r⟩)
 
 end iterator
 end string
@@ -201,7 +199,6 @@ private def line_column_aux : nat → string.iterator → nat × nat → nat ×
   else match it.curr with
        | '\n'  := line_column_aux k it.next (line+1, 0)
        | other := line_column_aux k it.next (line, col+1)
-       end
 
 def line_column (s : string) (offset : nat) : nat × nat :=
 line_column_aux offset s.mk_iterator (1, 0)
diff --git a/library/init/data/to_string.lean b/library/init/data/to_string.lean
index 069a1c9b58..f630f26222 100644
--- a/library/init/data/to_string.lean
+++ b/library/init/data/to_string.lean
@@ -62,10 +62,10 @@ instance : has_to_string uint64 :=
 ⟨λ n, to_string (fin.val n)⟩
 
 instance {α : Type u} [has_to_string α] : has_to_string (option α) :=
-⟨λ o, match o with | none := "none" | (some a) := "(some " ++ to_string a ++ ")" end⟩
+⟨λ o, match o with | none := "none" | (some a) := "(some " ++ to_string a ++ ")"⟩
 
 instance {α : Type u} {β : Type v} [has_to_string α] [has_to_string β] : has_to_string (α ⊕ β) :=
-⟨λ s, match s with | (inl a) := "(inl " ++ to_string a ++ ")" | (inr b) := "(inr " ++ to_string b ++ ")" end⟩
+⟨λ s, match s with | (inl a) := "(inl " ++ to_string a ++ ")" | (inr b) := "(inr " ++ to_string b ++ ")"⟩
 
 instance {α : Type u} {β : Type v} [has_to_string α] [has_to_string β] : has_to_string (α × β) :=
 ⟨λ ⟨a, b⟩, "(" ++ to_string a ++ ", " ++ to_string b ++ ")"⟩
diff --git a/library/init/lean/disjoint_set.lean b/library/init/lean/disjoint_set.lean
index 2c14a48b75..d0a2932538 100644
--- a/library/init/lean/disjoint_set.lean
+++ b/library/init/lean/disjoint_set.lean
@@ -33,7 +33,6 @@ private def find_aux : nat → α → hashmap α (node α) h → node α
   match m.find a with
   | some r := if r.find = a then r else find_aux n r.find m
   | none   := { find := a, rank := 0 }
-  end
 
 def find : disjoint_set α h → α → α
 | ⟨m⟩ a := (find_aux m.size a m).find
diff --git a/library/init/lean/ir/check.lean b/library/init/lean/ir/check.lean
index caeb9c1c3d..3b9e6d4ca7 100644
--- a/library/init/lean/ir/check.lean
+++ b/library/init/lean/ir/check.lean
@@ -141,8 +141,7 @@ p.ys.mfoldl (λ s y,
                    then do b ← read_block,
                            throw (ssa_error.phi_multiple_entries b.id p.x bid)
                    else return $ (s.insert bid)
-     | none   := do b ← read_block, throw (ssa_error.undefined b.id y)
-     end)
+     | none   := do b ← read_block, throw (ssa_error.undefined b.id y))
   mk_blockid_set
 
 def phis.check_predecessors (ps : list phi) : ssa_valid_m unit :=
@@ -152,8 +151,8 @@ do ps.mfoldl (λ (os : option blockid_set) (p : phi),
         | (some s) := if s.seteq s' then return os
                       else do b ← read_block,
                               throw (ssa_error.phi_missing_predecessor b.id p.x)
-        | none      := return (some s')
-     end) none,
+        | none      := return (some s'))
+     none,
    return ()
 
 def block.valid_ssa_core : ssa_valid_m unit :=
@@ -179,7 +178,6 @@ do m ← d.var2blockid,
       bs.mmap' (λ b : block, run_reader block.valid_ssa (m, b)),
       return m
    | _ := return m
-   end
 
 /- Check blockids -/
 inductive blockid_error
diff --git a/library/init/lean/name.lean b/library/init/lean/name.lean
index acbb1c28f6..224aaf263f 100644
--- a/library/init/lean/name.lean
+++ b/library/init/lean/name.lean
@@ -52,14 +52,12 @@ instance has_decidable_eq : decidable_eq name
     match has_decidable_eq p₁ p₂ with
     | is_true h₂  := is_true $ h₁ ▸ h₂ ▸ rfl
     | is_false h₂ := is_false $ λ h, name.no_confusion h $ λ hp hs, absurd hp h₂
-    end
   else is_false $ λ h, name.no_confusion h $ λ hp hs, absurd hs h₁
 | (mk_numeral p₁ n₁) (mk_numeral p₂ n₂) :=
   if h₁ : n₁ = n₂ then
     match has_decidable_eq p₁ p₂ with
     | is_true h₂  := is_true $ h₁ ▸ h₂ ▸ rfl
     | is_false h₂ := is_false $ λ h, name.no_confusion h $ λ hp hs, absurd hp h₂
-    end
   else is_false $ λ h, name.no_confusion h $ λ hp hs, absurd hs h₁
 | anonymous          (mk_string _ _)    := is_false $ λ h, name.no_confusion h
 | anonymous          (mk_numeral _ _)   := is_false $ λ h, name.no_confusion h
diff --git a/library/init/lean/parser/parser.lean b/library/init/lean/parser/parser.lean
index 31e49dfb5a..5d9b83e9c4 100644
--- a/library/init/lean/parser/parser.lean
+++ b/library/init/lean/parser/parser.lean
@@ -64,7 +64,6 @@ match p s.mk_iterator with
 | ok a _       := except.ok a
 | ok_eps a _ _ := except.ok a
 | error msg _  := except.error msg
-end
 
 @[inline] def mk_eps_result (a : α) (it : iterator) : result α :=
 ok_eps a it dlist.empty
@@ -91,19 +90,16 @@ def merge (msg₁ msg₂ : message) : message :=
 protected def bind (p : parser α) (q : α → parser β) : parser β :=
 λ it, match p it with
      | ok a it :=
-       match q a it with
-       | ok_eps b it msg₂ := ok b it
-       | error msg ff     := error msg tt
-       | other            := other
-       end
+       (match q a it with
+        | ok_eps b it msg₂ := ok b it
+        | error msg ff     := error msg tt
+        | other            := other)
      | ok_eps a it ex₁ :=
-       match q a it with
-       | ok_eps b it ex₂ := ok_eps b it (ex₁ ++ ex₂)
-       | error msg₂ ff   := error { expected := ex₁ ++ msg₂.expected, .. msg₂ } ff
-       | other           := other
-       end
+       (match q a it with
+        | ok_eps b it ex₂ := ok_eps b it (ex₁ ++ ex₂)
+        | error msg₂ ff   := error { expected := ex₁ ++ msg₂.expected, .. msg₂ } ff
+        | other           := other)
      | error msg c := error msg c
-     end
 
 instance : monad parser :=
 { bind := @parser.bind, pure := @parser.pure }
@@ -116,7 +112,6 @@ def expect (msg : message) (exp : string) : message :=
       | ok_eps a it _  := ok_eps a it (dlist.singleton ex)
       | error msg ff   := error (expect msg ex) ff
       | other          := other
-      end
 
 infixr ` <?> `:2 := label
 
@@ -141,7 +136,6 @@ def try (p : parser α) : parser α :=
 λ it, match p it with
       | error msg _  := error msg ff
       | other        := other
-      end
 
 /--
   The `orelse p q` combinator behaves as follows:
@@ -161,19 +155,16 @@ def try (p : parser α) : parser α :=
 protected def orelse (p q : parser α) : parser α :=
 λ it, match p it with
       | ok_eps a it' ex₁ :=
-        match q it with
-        | ok_eps _ _ ex₂ := ok_eps a it' (ex₁ ++ ex₂)
-        | error msg₂ ff  := ok_eps a it' (ex₁ ++ msg₂.expected)
-        | other          := other
-        end
+        (match q it with
+         | ok_eps _ _ ex₂ := ok_eps a it' (ex₁ ++ ex₂)
+         | error msg₂ ff  := ok_eps a it' (ex₁ ++ msg₂.expected)
+         | other          := other)
       | error msg₁ ff :=
-        match q it with
-        | ok_eps a it' ex₂ := ok_eps a it' (msg₁.expected ++ ex₂)
-        | error msg₂ ff    := error (merge msg₁ msg₂) ff
-        | other            := other
-        end
+        (match q it with
+         | ok_eps a it' ex₂ := ok_eps a it' (msg₁.expected ++ ex₂)
+         | error msg₂ ff    := error (merge msg₁ msg₂) ff
+         | other            := other)
       | other              := other
-      end
 
 instance : alternative parser :=
 { orelse  := @parser.orelse,
@@ -400,7 +391,6 @@ def lookahead (p : parser α) : parser α :=
 λ it, match p it with
       | ok a s' := mk_eps_result a it
       | other   := other
-      end
 
 /-- `not_followed_by p` succeeds when parser `p` fails -/
 def not_followed_by (p : parser α) (msg : string := "input") : parser unit :=
@@ -408,7 +398,6 @@ def not_followed_by (p : parser α) (msg : string := "input") : parser unit :=
       | ok _ _       := error { pos := it.offset, unexpected := msg } ff
       | ok_eps _ _ _ := error { pos := it.offset, unexpected := msg } ff
       | error _ _    := mk_eps_result () it
-      end
 
 /-- Faster version of `not_followed_by (satisfy p)` -/
 @[inline] def not_followed_by_sat (p : char → bool) : parser unit :=
diff --git a/library/init/meta/contradiction_tactic.lean b/library/init/meta/contradiction_tactic.lean
index cb4c422f14..d032995e41 100644
--- a/library/init/meta/contradiction_tactic.lean
+++ b/library/init/meta/contradiction_tactic.lean
@@ -68,7 +68,6 @@ private meta def contra_constructor_eq : list expr → tactic unit
                   exact pr
           else contra_constructor_eq Hs
      | _ := contra_constructor_eq Hs
-     end
 
 meta def contradiction : tactic unit :=
 do try intro1,
diff --git a/library/init/meta/decl_cmds.lean b/library/init/meta/decl_cmds.lean
index 56cb738e60..46e7c8e47e 100644
--- a/library/init/meta/decl_cmds.lean
+++ b/library/init/meta/decl_cmds.lean
@@ -11,12 +11,10 @@ private meta def apply_replacement (replacements : name_map name) (e : expr) : e
 e.replace (λ e d,
   match e with
   | expr.const n ls :=
-    match replacements.find n with
-    | some new_n := some (expr.const new_n ls)
-    | none       := none
-    end
-  | _ := none
-  end)
+    (match replacements.find n with
+     | some new_n := some (expr.const new_n ls)
+     | none       := none)
+  | _ := none)
 
 /-- Given a set of constant renamings `replacements` and a declaration name `src_decl_name`, create a new
    declaration called `new_decl_name` s.t. its type is the type of `src_decl_name` after applying the
diff --git a/library/init/meta/environment.lean b/library/init/meta/environment.lean
index c303b7f5d5..8ac3ef8f17 100644
--- a/library/init/meta/environment.lean
+++ b/library/init/meta/environment.lean
@@ -35,7 +35,7 @@ meta def      contains (env : environment) (d : name) : bool :=
 match env.get d with
 | exceptional.success _      := tt
 | exceptional.exception ._ _ := ff
-end
+
 /-- Register the given name as a namespace, making it available to the `open` command -/
 meta constant add_namespace   : environment → name → environment
 /-- Return tt iff the given name is a namespace -/
@@ -105,7 +105,6 @@ match (refl_for env (const_name (get_app_fn e))) with
     then some (n, app_arg (app_fn e), app_arg e)
     else none
 | none   := none
-end
 
 /-- Return true if 'n' has been declared in the current file -/
 meta def in_current_file (env : environment) (n : name) : bool :=
@@ -115,7 +114,6 @@ meta def is_definition (env : environment) (n : name) : bool :=
 match env.get n with
 | exceptional.success (declaration.defn _ _ _ _ _ _) := tt
 | _                                                  := ff
-end
 
 end environment
 
diff --git a/library/init/meta/expr.lean b/library/init/meta/expr.lean
index b70714e2a4..17c43f7ae6 100644
--- a/library/init/meta/expr.lean
+++ b/library/init/meta/expr.lean
@@ -29,8 +29,7 @@ instance : has_repr binder_info :=
 | binder_info.implicit := "implicit"
 | binder_info.strict_implicit := "strict_implicit"
 | binder_info.inst_implicit := "inst_implicit"
-| binder_info.aux_decl := "aux_decl"
-end⟩
+| binder_info.aux_decl := "aux_decl"⟩
 
 meta constant macro_def : Type
 
@@ -64,7 +63,6 @@ meta def expr.erase_annotations : expr elab → expr elab
   match e.is_annotation with
   | some (_, a) := expr.erase_annotations a
   | none        := e
-  end
 
 /-- Compares expressions, including binder names. -/
 meta constant expr.has_decidable_eq : decidable_eq expr
@@ -147,7 +145,6 @@ id
 λ ef ea, match ef with
 | (expr.lam _ _ _ _) := expr.subst ef ea
 | _                  := expr.app   ef ea
-end
 
 attribute [irreducible] reflected reflected.subst reflected.to_expr
 
diff --git a/library/init/meta/injection_tactic.lean b/library/init/meta/injection_tactic.lean
index 09323218da..da6f279d08 100644
--- a/library/init/meta/injection_tactic.lean
+++ b/library/init/meta/injection_tactic.lean
@@ -73,7 +73,6 @@ private meta def injections_with_inner : nat → list expr → list name → tac
   | none          := injections_with_inner (n+1) lc ns
   | some ([], _)  := skip -- This means that the contradiction part was triggered and the goal is done
   | some (t, ns') := injections_with_inner n (t ++ lc) ns'
-  end
 
 meta def injections_with (ns : list name) : tactic unit :=
 do lc ← local_context,
diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean
index eb6bdbfa5f..4b8d64bbd8 100644
--- a/library/init/meta/interactive.lean
+++ b/library/init/meta/interactive.lean
@@ -73,12 +73,10 @@ let aux (n : name) : tactic expr := do
   match p with
   | (expr.const c []) := do r ← mk_const c, save_type_info r q, return r
   | _                 := i_to_expr p
-  end
 in match q with
 | (expr.const c [])          := aux c
 | (expr.local_const c _ _ _) := aux c
 | _                          := i_to_expr q
-end
 
 namespace interactive
 open interactive interactive.types expr
@@ -108,8 +106,7 @@ mcond tags_enabled
       r ← r.mfilter $ λ ⟨n, m⟩, bnot <$> is_assigned m,
       match r with
       | [(_, m)] := set_tag m in_tag /- if there is only new subgoal, we just propagate `in_tag` -/
-      | _        := r.mmap' (λ ⟨n, m⟩, set_tag m (n::in_tag))
-      end)
+      | _        := r.mmap' (λ ⟨n, m⟩, set_tag m (n::in_tag)))
   (tac >> skip)
 
 /--
@@ -289,9 +286,7 @@ do {
   p ← resolve_name n,
   match p with
   | expr.const n _ := mk_const n -- create metavars for universe levels
-  | _              := i_to_expr p
-  end
-}
+  | _              := i_to_expr p }
 
 /- Version of to_expr that tries to bypass the elaborator if `p` is just a constant or local constant.
    This is not an optimization, by skipping the elaborator we make sure that no unwanted resolution is used.
@@ -302,7 +297,6 @@ match p with
 | (const c [])          := do new_e ← resolve_name' c, save_type_info new_e p, return new_e
 | (local_const c _ _ _) := do new_e ← resolve_name' c, save_type_info new_e p, return new_e
 | _                     := i_to_expr p
-end
 
 meta structure rw_rule :=
 (pos  : pos)
@@ -319,13 +313,11 @@ let aux (n : name) : tactic (list name) := do {
   let e := p.erase_annotations.get_app_fn.erase_annotations,
   match e with
   | const n _ := get_eqn_lemmas_for tt n
-  | _         := return []
-  end } <|> return [] in
+  | _         := return [] } <|> return [] in
 match r.rule with
 | const n _           := aux n
 | local_const n _ _ _ := aux n
 | _                   := return []
-end
 
 private meta def rw_goal (cfg : rewrite_cfg) (rs : list rw_rule) : tactic unit :=
 rs.mmap' $ λ r, do
@@ -367,11 +359,11 @@ meta def rw_rules : parser rw_rules_t :=
 <|> rw_rules_t.mk <$> (list.ret <$> rw_rule_p texpr) <*> return none
 
 private meta def rw_core (rs : parse rw_rules) (loca : parse location) (cfg : rewrite_cfg) : tactic unit :=
-match loca with
-| loc.wildcard := loca.try_apply (rw_hyp cfg rs.rules) (rw_goal cfg rs.rules)
-| _            := loca.apply (rw_hyp cfg rs.rules) (rw_goal cfg rs.rules)
-end >> try (reflexivity reducible)
-    >> (returnopt rs.end_pos >>= save_info <|> skip)
+(match loca with
+ | loc.wildcard := loca.try_apply (rw_hyp cfg rs.rules) (rw_goal cfg rs.rules)
+ | _            := loca.apply (rw_hyp cfg rs.rules) (rw_goal cfg rs.rules))
+>> try (reflexivity reducible)
+>> (returnopt rs.end_pos >>= save_info <|> skip)
 
 /--
 `rewrite e` applies identity `e` as a rewrite rule to the target of the main goal. If `e` is preceded by left arrow (`←` or `<-`), the rewrite is applied in the reverse direction. If `e` is a defined constant, then the equational lemmas associated with `e` are used. This provides a convenient way to unfold `e`.
@@ -486,7 +478,6 @@ with_desc "(id :)? expr" $ do
   | (local_const x _ _ _) :=
     (tk ":" *> do t ← texpr, pure (some x, t)) <|> pure (none, t)
   | _ := pure (none, t)
-  end
 
 /--
   Given the initial tag `in_tag` and the cases names produced by `induction` or `cases` tactic,
@@ -509,7 +500,6 @@ do te ← tags_enabled,
              ```
           -/
      else tgs.mmap' (λ ⟨n, g⟩, with_enable_tags (set_tag g (`_case_simple::n::[])))
-   end
 
 private meta def set_induction_tags (in_tag : tag) (rs : list (name × list expr × list (name × expr))) : tactic unit :=
 set_cases_tags in_tag (rs.map (λ e, e.1))
@@ -534,14 +524,12 @@ meta def induction (hp : parse cases_arg_p) (rec_name : parse using_ident) (ids
 do in_tag ← get_main_tag,
 focus1 $ do {
     -- process `h : t` case
-    e ← match hp with
-       | (some h, p) := do
-         x ← get_unused_name,
-         generalize h () (p, x),
-         get_local x
-       | (none, p) := i_to_expr p
-       end,
-
+    e ← (match hp with
+         | (some h, p) := do
+           x ← get_unused_name,
+           generalize h () (p, x),
+           get_local x
+         | (none, p) := i_to_expr p),
    -- generalize major premise
    e ← if e.is_local_constant then pure e
        else tactic.generalize e >> intro1,
@@ -612,7 +600,6 @@ do gs ← collect_tagged_goals pre,
    | gs  := do
      tags : list (list name) ← gs.mmap get_tag,
      fail ("invalid `case`, there is more than one goal tagged with prefix " ++ to_string pre ++ ", matching tags: " ++ to_string tags)
-   end
 
 private meta def find_tagged_goal (pre : list name) : tactic expr :=
 match pre with
@@ -628,7 +615,6 @@ match pre with
                else return r_id)
             <|> return id),
      find_tagged_goal_aux pre
-end
 
 private meta def find_case (goals : list expr) (ty : name) (idx : nat) (num_indices : nat) : option expr → expr → option (expr × expr)
 | case e := if e.has_meta_var then match e with
@@ -638,34 +624,30 @@ private meta def find_case (goals : list expr) (ty : name) (idx : nat) (num_indi
        pure (case, e)
   | (app _ _)    :=
     let idx :=
-      match e.get_app_fn with
+     (match e.get_app_fn with
       | const (name.mk_string rec ty') _ :=
         guard (ty' = ty) >>
-        match mk_simple_name rec with
-        | `drec := some idx | `rec := some idx
-        -- indices + major premise
-        | `dcases_on := some (idx + num_indices + 1) | `cases_on := some (idx + num_indices + 1)
-        | _ := none
-        end
-      | _ := none
-      end in
-    match idx with
-    | none := list.foldl (<|>) (find_case case e.get_app_fn) $ e.get_app_args.map (find_case case)
-    | some idx :=
-      let args := e.get_app_args in
-      do arg ← args.nth idx,
+        (match mk_simple_name rec with
+         | `drec := some idx | `rec := some idx
+         -- indices + major premise
+         | `dcases_on := some (idx + num_indices + 1) | `cases_on := some (idx + num_indices + 1)
+         | _ := none)
+      | _ := none) in
+    (match idx with
+     | none := list.foldl (<|>) (find_case case e.get_app_fn) $ e.get_app_args.map (find_case case)
+     | some idx :=
+       let args := e.get_app_args in
+       do arg ← args.nth idx,
          args.enum.foldl
            (λ acc ⟨i, arg⟩, match acc with
              | some _ := acc
-             | _      := if i ≠ idx then find_case none arg else none
-             end)
+             | _      := if i ≠ idx then find_case none arg else none)
            -- start recursion with likely case
-           (find_case (some arg) arg)
-    end
+           (find_case (some arg) arg))
   | (lam _ _ _ e) := find_case case e
   | (macro n args) := list.foldl (<|>) none $ args.map (find_case case)
   | _             := none
-  end else none
+  else none
 
 private meta def rename_lams : expr → list name → tactic unit
 | (lam n _ _ e) (n'::ns) := (rename n n' >> rename_lams e ns) <|> rename_lams e (n'::ns)
@@ -718,8 +700,6 @@ do g   ← find_tagged_goal pre,
           rename_lams case ids,
           solve1 tac
      | ff := failed
-     end
-   end
 
 /--
 Assuming `x` is a variable in the local context with an inductive type, `destruct x` splits the main goal, producing one goal for each constructor of the inductive type, in which `x` is assumed to be a general instance of that constructor. In contrast to `cases`, the local context is unchanged, i.e. no elements are reverted or introduced.
@@ -838,7 +818,6 @@ meta def iterate (n : parse small_nat?) (t : itactic) : tactic unit :=
 match n with
 | none   := tactic.iterate t
 | some n := iterate_exactly n t
-end
 
 /--
 `repeat { t }` applies `t` to each goal. If the application succeeds,
@@ -920,7 +899,7 @@ If `h` is omitted, the name `this` is used.
 -/
 meta def «have» (h : parse ident?) (q₁ : parse (tk ":" *> texpr)?) (q₂ : parse $ (tk ":=" *> texpr)?) : tactic unit :=
 let h := h.get_or_else `this in
-match q₁, q₂ with
+(match q₁, q₂ with
 | some e, some p := do
   t ← i_to_expr e,
   v ← i_to_expr ``(%%p : %%t),
@@ -932,8 +911,8 @@ match q₁, q₂ with
 | none, none := do
   u ← mk_meta_univ,
   e ← mk_meta_var (sort u),
-  tactic.assert h e
-end >> skip
+  tactic.assert h e)
+>> skip
 
 /--
 `let h : t := p` adds the hypothesis `h : t := p` to the current goal if `p` a term of type `t`. If `t` is omitted, it will be inferred.
@@ -944,20 +923,20 @@ If `h` is omitted, the name `this` is used.
 -/
 meta def «let» (h : parse ident?) (q₁ : parse (tk ":" *> texpr)?) (q₂ : parse $ (tk ":=" *> texpr)?) : tactic unit :=
 let h := h.get_or_else `this in
-match q₁, q₂ with
-| some e, some p := do
-  t ← i_to_expr e,
-  v ← i_to_expr ``(%%p : %%t),
-  tactic.definev h t v
-| none, some p := do
-  p ← i_to_expr p,
-  tactic.pose h none p
-| some e, none := i_to_expr e >>= tactic.define h
-| none, none := do
-  u ← mk_meta_univ,
-  e ← mk_meta_var (sort u),
-  tactic.define h e
-end >> skip
+(match q₁, q₂ with
+ | some e, some p := do
+   t ← i_to_expr e,
+   v ← i_to_expr ``(%%p : %%t),
+   tactic.definev h t v
+ | none, some p := do
+   p ← i_to_expr p,
+   tactic.pose h none p
+ | some e, none := i_to_expr e >>= tactic.define h
+ | none, none := do
+   u ← mk_meta_univ,
+   e ← mk_meta_var (sort u),
+   tactic.define h e)
+>> skip
 
 /--
 `suffices h : t` is the same as `have h : t, tactic.swap`. In other words, it adds the hypothesis `h : t` to the current goal and opens a new subgoal with target `t`.
@@ -1080,7 +1059,6 @@ private meta def resolve_exception_ids (all_hyps : bool) : list name → list na
   | local_const n _ _ _ := when (not all_hyps) (fail $ sformat! "invalid local exception {id}, '*' was not used") >>
                            resolve_exception_ids ids gex (n::hex)
   | _                   := fail $ sformat! "invalid exception {id}, unknown identifier"
-  end
 
 /- Return (hs, gex, hex, all) -/
 meta def decode_simp_arg_list (hs : list simp_arg_type) : tactic $ list pexpr × list name × list name × bool :=
@@ -1090,8 +1068,7 @@ do
        match r, h with
        | (es, ex, all), simp_arg_type.all_hyps  := (es, ex, tt)
        | (es, ex, all), simp_arg_type.except id := (es, id::ex, all)
-       | (es, ex, all), simp_arg_type.expr e    := (e::es, ex, all)
-       end)
+       | (es, ex, all), simp_arg_type.expr e    := (e::es, ex, all))
     ([], [], ff),
   (gex, hex) ← resolve_exception_ids all ex [] [],
   return (hs.reverse, gex, hex, all)
@@ -1110,7 +1087,6 @@ when p.is_choice_macro $
     fail $ to_fmt "ambiguous overload, possible interpretations" ++
            format.join (ps.map (λ p, (to_fmt p).indent 4))
   | _ := failed
-  end
 
 private meta def simp_lemmas.resolve_and_add (s : simp_lemmas) (u : list name) (n : name) (ref : pexpr) : tactic (simp_lemmas × list name) :=
 do
@@ -1131,14 +1107,12 @@ do
     (do e ← i_to_expr_no_subgoals p, b ← is_valid_simp_lemma e, guard b, try (save_type_info e ref), s ← s.add e, return (s, u))
     <|>
     report_invalid_simp_lemma n
-  end
 
 private meta def simp_lemmas.add_pexpr (s : simp_lemmas) (u : list name) (p : pexpr) : tactic (simp_lemmas × list name) :=
 match p with
 | (const c [])          := simp_lemmas.resolve_and_add s u c p
 | (local_const c _ _ _) := simp_lemmas.resolve_and_add s u c p
 | _                     := do new_e ← i_to_expr_no_subgoals p, s ← s.add new_e, return (s, u)
-end
 
 private meta def simp_lemmas.append_pexprs : simp_lemmas → list name → list pexpr → tactic (simp_lemmas × list name)
 | s u []      := return (s, u)
@@ -1181,14 +1155,13 @@ do to_remove ← hs.mfilter $ λ h, do {
 meta def simp_core (cfg : simp_config) (discharger : tactic unit)
                    (no_dflt : bool) (hs : list simp_arg_type) (attr_names : list name)
                    (locat : loc) : tactic unit :=
-match locat with
-| loc.wildcard := do (all_hyps, s, u) ← mk_simp_set_core no_dflt attr_names hs tt,
-                     if all_hyps then tactic.simp_all s u cfg discharger
-                     else do hyps ← non_dep_prop_hyps, simp_core_aux cfg discharger s u hyps tt
-| _            := do (s, u) ← mk_simp_set no_dflt attr_names hs,
-                     ns ← locat.get_locals,
-                     simp_core_aux cfg discharger s u ns locat.include_goal
-end
+(match locat with
+ | loc.wildcard := do (all_hyps, s, u) ← mk_simp_set_core no_dflt attr_names hs tt,
+                      if all_hyps then tactic.simp_all s u cfg discharger
+                      else do hyps ← non_dep_prop_hyps, simp_core_aux cfg discharger s u hyps tt
+ | _            := do (s, u) ← mk_simp_set no_dflt attr_names hs,
+                      ns ← locat.get_locals,
+                      simp_core_aux cfg discharger s u ns locat.include_goal)
 >> try tactic.triv >> try (tactic.reflexivity reducible)
 
 /--
@@ -1257,7 +1230,6 @@ match l with
      dsimp_target s u {zeta := ff ..cfg},
      intron n
 | _ := l.apply (λ h, dsimp_hyp h s u cfg) (dsimp_target s u cfg)
-end
 
 /--
 This tactic applies to a goal whose target has the form `t ~ u` where `~` is a reflexive relation, that is, a relation which has a reflexivity lemma tagged with the attribute `[refl]`. The tactic checks whether `t` and `u` are definitionally equal and then solves the goal.
@@ -1288,7 +1260,6 @@ tactic.transitivity >> match q with
 | some q :=
   do (r, lhs, rhs) ← target_lhs_rhs,
      i_to_expr q >>= unify rhs
-end
 
 /--
 Given hypothesis `h : x = t` or `h : t = x`, where `x` is a local constant, `subst h` substitutes `x` by `t` everywhere in the main goal and then clears `h`.
@@ -1338,7 +1309,6 @@ match l with
                           dunfold_target new_cs cfg,
                           intron n
 | _              := do new_cs ← to_qualified_names cs, l.apply (λ h, dunfold_hyp cs h cfg) (dunfold_target new_cs cfg)
-end
 
 private meta def delta_hyps : list name → list name → tactic unit
 | cs []      := skip
@@ -1370,7 +1340,6 @@ match l with
 | _            :=
   l.try_apply (λ h, unfold_projs_hyp h cfg)
     (tactic.unfold_projs_target cfg) <|> fail "unfold_projs failed to simplify"
-end
 
 end interactive
 
diff --git a/library/init/meta/interactive_base.lean b/library/init/meta/interactive_base.lean
index 65318dd67b..4ba091c1f9 100644
--- a/library/init/meta/interactive_base.lean
+++ b/library/init/meta/interactive_base.lean
@@ -35,8 +35,8 @@ meta def loc.get_locals : loc → tactic (list expr)
 | loc.wildcard := tactic.local_context
 | (loc.ns xs)  := xs.mfoldl (λ ls n, match n with
   | none := pure ls
-  | some n := do l ← tactic.get_local n, pure $ l :: ls
-  end) []
+  | some n := do l ← tactic.get_local n, pure $ l :: ls)
+  []
 
 meta def loc.apply (hyp_tac : expr → tactic unit) (goal_tac : tactic unit) (l : loc) : tactic unit :=
 do hs ← l.get_locals,
diff --git a/library/init/meta/rb_map.lean b/library/init/meta/rb_map.lean
index c69e4ee46e..67806fe58f 100644
--- a/library/init/meta/rb_map.lean
+++ b/library/init/meta/rb_map.lean
@@ -121,7 +121,6 @@ meta def insert {key : Type} {data : Type} (rbl : rb_lmap key data) (k : key) (d
 match (rb_map.find rbl k) with
 | none     := rb_map.insert rbl k [d]
 | (some l) := rb_map.insert (rb_map.erase rbl k) k (d :: l)
-end
 
 meta def erase {key : Type} {data : Type} (rbl : rb_lmap key data) (k : key) :
   rb_lmap key data :=
@@ -134,7 +133,6 @@ meta def find {key : Type} {data : Type} (rbl : rb_lmap key data) (k : key) : li
 match (rb_map.find rbl k) with
 | none     := []
 | (some l) := l
-end
 
 end rb_lmap
 
diff --git a/library/init/meta/rec_util.lean b/library/init/meta/rec_util.lean
index f832f5316e..8aef15ddd2 100644
--- a/library/init/meta/rec_util.lean
+++ b/library/init/meta/rec_util.lean
@@ -58,7 +58,7 @@ private meta def mk_constructors_arg_names_aux : list name → name → nat →
 | []      p i r := return (list.reverse r)
 | (c::cs) p i r := do
   v : list name × nat ← mk_constructor_arg_names c p i,
-  match v with (l, i') := mk_constructors_arg_names_aux cs p i' (l :: r) end
+  match v with (l, i') := mk_constructors_arg_names_aux cs p i' (l :: r)
 
 /-- Given an inductive datatype I with k constructors and where constructor i has n_i fields,
    return the list [[p.1, ..., p.n_1], [p.{n_1 + 1}, ..., p.{n_1 + n_2}], ..., [..., p.{n_1 + ... + n_k}]] -/
@@ -99,7 +99,6 @@ private meta def mk_constructor_fresh_names_aux : nat → expr → name_set →
        mk_constructor_fresh_names_aux (nparams - 1) ty' s
      }
   | _ := return ([], s)
-  end
 
 meta def mk_constructor_fresh_names (nparams : nat) (c : name) (s : name_set) : tactic (list name × name_set) :=
 do d    ← get_decl c,
diff --git a/library/init/meta/relation_tactics.lean b/library/init/meta/relation_tactics.lean
index 8da8a8155e..063c450da3 100644
--- a/library/init/meta/relation_tactics.lean
+++ b/library/init/meta/relation_tactics.lean
@@ -16,7 +16,6 @@ do tgt   ← target >>= instantiate_mvars,
    match (op_for env (const_name r)) with
    | (some refl) := do r ← mk_const refl, apply_core r {md := md, new_goals := new_goals.non_dep_only} >> return ()
    | none        := fail $ tac_name ++ " tactic failed, target is not a relation application with the expected property."
-   end
 
 meta def reflexivity (md := semireducible) : tactic unit :=
 relation_tactic md environment.refl_for "reflexivity"
diff --git a/library/init/meta/simp_tactic.lean b/library/init/meta/simp_tactic.lean
index 8742e861e8..6f0dff09e8 100644
--- a/library/init/meta/simp_tactic.lean
+++ b/library/init/meta/simp_tactic.lean
@@ -53,15 +53,14 @@ namespace tactic
 meta def revert_and_transform (transform : expr → tactic expr) (h : expr) : tactic unit :=
 do num_reverted : ℕ ← revert h,
    t ← target,
-   match t with
-   | expr.pi n bi d b  :=
-        do h_simp ← transform d,
-           unsafe_change $ expr.pi n bi h_simp b
-   | expr.elet n g e f :=
-        do h_simp ← transform g,
-           unsafe_change $ expr.elet n h_simp e f
-   | _ := fail "reverting hypothesis created neither a pi nor an elet expr (unreachable?)"
-   end,
+   (match t with
+    | expr.pi n bi d b  :=
+         do h_simp ← transform d,
+            unsafe_change $ expr.pi n bi h_simp b
+    | expr.elet n g e f :=
+         do h_simp ← transform g,
+            unsafe_change $ expr.elet n h_simp e f
+    | _ := fail "reverting hypothesis created neither a pi nor an elet expr (unreachable?)"),
    intron num_reverted
 
 /-- `get_eqn_lemmas_for deps d` returns the automatically generated equational lemmas for definition d.
@@ -274,7 +273,7 @@ meta constant ext_simplify_core
 
 private meta def is_equation : expr → bool
 | (expr.pi n bi d b) := is_equation b
-| e                  := match (expr.is_eq e) with (some a) := tt | none := ff end
+| e                  := match (expr.is_eq e) with | (some a) := tt | none := ff
 
 meta def collect_ctx_simps : tactic (list expr) :=
 local_context
@@ -447,7 +446,6 @@ es.mmap' $ λ e,
    | some pr :=
       assert e.h.local_pp_name e.new_type >>
       mk_eq_mp pr e.h >>= exact
-   end
 
 private meta def clear_old_hyps (es : list simp_all_entry) : tactic unit :=
 es.mmap' $ λ e, when (e.pr ≠ none) (try (clear e.h))
diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index 08b3b08386..6fa3c89e31 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -65,13 +65,11 @@ meta def {u₁ u₂} tactic.up {α : Type u₂} (t : tactic α) : tactic (ulift.
 λ s, match t s with
 | success a s'      := success (ulift.up a) s'
 | exception t ref s := exception t ref s
-end
 
 meta def {u₁ u₂} tactic.down {α : Type u₂} (t : tactic (ulift.{u₁} α)) : tactic α :=
 λ s, match t s with
 | success (ulift.up a) s' := success a s'
 | exception t ref s       := exception t ref s
-end
 
 namespace tactic
 variables {α : Type u}
@@ -96,8 +94,6 @@ meta def try_lst : list (tactic unit) → tactic unit
     match try_lst tacs s' with
     | result.exception _ _ _ := result.exception e p s'
     | r := r
-    end
-  end
 
 meta def fail_if_success {α : Type u} (t : tactic α) : tactic unit :=
 λ s, result.cases_on (t s)
@@ -109,7 +105,6 @@ meta def success_if_fail {α : Type u} (t : tactic α) : tactic unit :=
 | (interaction_monad.result.exception _ _ s') := success () s
 | (interaction_monad.result.success a s) :=
    mk_exception "success_if_fail combinator failed, given tactic succeeded" none s
-end
 
 open nat
 /-- (iterate_at_most n t): repeat the given tactic at most n times or until t fails -/
@@ -129,7 +124,6 @@ meta def returnopt (e : option α) : tactic α :=
 λ s, match e with
 | (some a) := success a s
 | none     := mk_exception "failed" none s
-end
 
 meta instance opt_to_tac : has_coe (option α) (tactic α) :=
 ⟨returnopt⟩
@@ -141,8 +135,7 @@ meta def decorate_ex (msg : format) (t : tactic α) : tactic α :=
   (λ opt_thunk,
      match opt_thunk with
      | some e := exception (some (λ u, msg ++ format.nest 2 (format.line ++ e u)))
-     | none   := exception none
-     end)
+     | none   := exception none)
 
 @[inline] meta def write (s' : tactic_state) : tactic unit :=
 λ s, success () s'
@@ -169,8 +162,6 @@ meta def returnex {α : Type} (e : exceptional α) : tactic α :=
   match get_options s with
   | success opt _   := exception (some (λ u, f opt)) none s
   | exception _ _ _ := exception (some (λ u, f options.mk)) none s
-  end
-end
 
 meta instance ex_to_tac {α : Type} : has_coe (exceptional α) (tactic α) :=
 ⟨returnex⟩
@@ -594,7 +585,6 @@ match t with
 | expr.pi   _ _ _ _ := do H ← intro1, Hs ← intros, return (H :: Hs)
 | expr.elet _ _ _ _ := do H ← intro1, Hs ← intros, return (H :: Hs)
 | _                 := return []
-end
 
 meta def intro_lst : list name → tactic (list expr)
 | []      := return []
@@ -613,7 +603,6 @@ do t ← target,
    | expr.pi _ _ _ b   := proc b
    | expr.elet _ _ _ b := proc b
    | _                 := return []
-   end
 
 meta def introv : list name → tactic (list expr)
 | []      := intros_dep
@@ -642,7 +631,6 @@ do lctx ← local_context,
    | some []        := revert_lst lctx
                        /- `hi` is the last local instance. We shoul truncate `lctx` at `hi`. -/
    | some (hi::his) := revert_lst $ lctx.foldl (λ r h, if h.local_uniq_name = hi.local_uniq_name then [] else h :: r) []
-   end
 
 meta def clear_lst : list name → tactic unit
 | []      := skip
@@ -652,50 +640,42 @@ meta def match_not (e : expr) : tactic expr :=
 match (expr.is_not e) with
 | (some a) := return a
 | none     := fail "expression is not a negation"
-end
 
 meta def match_and (e : expr) : tactic (expr × expr) :=
 match (expr.is_and e) with
 | (some (α, β)) := return (α, β)
 | none     := fail "expression is not a conjunction"
-end
 
 meta def match_or (e : expr) : tactic (expr × expr) :=
 match (expr.is_or e) with
 | (some (α, β)) := return (α, β)
 | none     := fail "expression is not a disjunction"
-end
 
 meta def match_iff (e : expr) : tactic (expr × expr) :=
 match (expr.is_iff e) with
 | (some (lhs, rhs)) := return (lhs, rhs)
 | none              := fail "expression is not an iff"
-end
 
 meta def match_eq (e : expr) : tactic (expr × expr) :=
 match (expr.is_eq e) with
 | (some (lhs, rhs)) := return (lhs, rhs)
 | none              := fail "expression is not an equality"
-end
 
 meta def match_ne (e : expr) : tactic (expr × expr) :=
 match (expr.is_ne e) with
 | (some (lhs, rhs)) := return (lhs, rhs)
 | none              := fail "expression is not a disequality"
-end
 
 meta def match_heq (e : expr) : tactic (expr × expr × expr × expr) :=
 do match (expr.is_heq e) with
 | (some (α, lhs, β, rhs)) := return (α, lhs, β, rhs)
 | none                    := fail "expression is not a heterogeneous equality"
-end
 
 meta def match_refl_app (e : expr) : tactic (name × expr × expr) :=
 do env ← get_env,
 match (environment.is_refl_app env e) with
 | (some (R, lhs, rhs)) := return (R, lhs, rhs)
 | none                 := fail "expression is not an application of a reflexive relation"
-end
 
 meta def match_app_of (e : expr) (n : name) : tactic (list expr) :=
 guard (expr.is_app_of e n) >> return e.get_app_args
@@ -745,7 +725,6 @@ do gs ← get_goals,
    match gs with
    | (g₁ :: g₂ :: rs) := set_goals (g₂ :: g₁ :: rs)
    | e                := skip
-   end
 
 /-- `assert h t`, adds a new goal for t, and the hypothesis `h : t` in the current goal. -/
 meta def assert (h : name) (t : expr) : tactic expr :=
@@ -797,7 +776,6 @@ private meta def repeat_aux (t : tactic unit) : list expr → list expr → tact
   | _    := do
     gs' ← get_goals,
     repeat_aux (gs' ++ gs) r
-  end
 
 /-- This tactic is applied to each goal. If the application succeeds,
     the tactic is applied recursively to all the generated subgoals until it eventually fails.
@@ -824,8 +802,6 @@ do gs ← get_goals,
         match gs' with
         | [] := set_goals rs
         | gs := fail "solve1 tactic failed, focused goal has not been solved"
-        end
-   end
 
 /-- `solve [t_1, ... t_n]` applies the first tactic that solves the main goal. -/
 meta def solve (ts : list (tactic unit)) : tactic unit :=
@@ -856,7 +832,6 @@ do g::gs ← get_goals,
       gs' ← get_goals,
       set_goals (gs' ++ gs),
       return a
-   end
 
 private meta def all_goals_core (tac : tactic unit) : list expr → list expr → tactic unit
 | []        ac := set_goals ac
@@ -1074,7 +1049,6 @@ do tgt : expr ← target,
    match H with
    | some n := intro n
    | none   := intro1
-   end
 
 private meta def generalizes_aux (md : transparency) : list expr → tactic unit
 | []      := skip
@@ -1208,7 +1182,6 @@ meta def try_for {α} (max : nat) (tac : tactic α) : tactic α :=
 match _root_.try_for max (tac s) with
 | some r := r
 | none   := mk_exception "try_for tactic failed, timeout" none s
-end
 
 meta def updateex_env (f : environment → exceptional environment) : tactic unit :=
 do env ← get_env,
@@ -1288,7 +1261,6 @@ meta def any_of {α β} : list α → (α → tactic β) → tactic β
                    match opt_b with
                    | some b := return b
                    | none   := any_of es fn
-                   end
 end list
 
 /- Install monad laws tactic and use it to prove some instances. -/
diff --git a/library/system/io.lean b/library/system/io.lean
index 929fe49f2a..0855ac622a 100644
--- a/library/system/io.lean
+++ b/library/system/io.lean
@@ -52,7 +52,6 @@ cleanup,
 match res with
 | sum.inr res := return res
 | sum.inl error := monad_io.fail _ _ _ error
-end
 
 protected def fail {α : Type} (s : string) : io α :=
 monad_io.fail io_core _ _ (io.error.other s)
diff --git a/src/frontends/lean/match_expr.cpp b/src/frontends/lean/match_expr.cpp
index 0b95ead269..201176a3c2 100644
--- a/src/frontends/lean/match_expr.cpp
+++ b/src/frontends/lean/match_expr.cpp
@@ -81,10 +81,6 @@ expr parse_match(parser & p, unsigned, expr const *, pos_info const & pos) {
         consume_until_end_or_command(p);
         ex.rethrow();
     }
-    if (p.curr_is_token(get_end_tk())) {
-        // TODO(Sebastian): legacy syntax, remove
-        p.next();
-    }
     expr f = p.save_pos(mk_equations(header, eqns.size(), eqns.data()), pos);
     return p.mk_app(f, ts, pos);
 }
diff --git a/tests/lean/parser1.lean b/tests/lean/parser1.lean
index cbaeb088d9..8a6e27a362 100644
--- a/tests/lean/parser1.lean
+++ b/tests/lean/parser1.lean
@@ -5,19 +5,16 @@ def test {α} [decidable_eq α] (p : parser α) (s : string) (e : α) : io unit
 match parse p s with
 | except.ok a    := if a = e then return () else io.print_ln "unexpected result"
 | except.error e := io.print_ln (e.to_string s)
-end
 
 def test_failure {α} (p : parser α) (s : string) : io unit :=
 match parse p s with
 | except.ok a    := io.print_ln "unexpected success"
 | except.error e := return ()
-end
 
 def show_result {α} [has_to_string α] (p : parser α) (s : string) : io unit :=
 match parse p s with
 | except.ok a    := io.print_ln "result: " >> io.print_ln (repr $ to_string a)
 | except.error e := io.print_ln (e.to_string s)
-end
 
 #eval test (ch 'a') "a" 'a'
 #eval test any "a" 'a'
@@ -149,12 +146,10 @@ instance eq_expr : decidable_eq Expr
 | (Add e₁ e₂) (Var y)     := is_false (λ h, Expr.no_confusion h)
 | (Add e₁ e₂) (Add e₃ e₄) :=
   match eq_expr e₁ e₃ with
-  | is_true h   := match eq_expr e₂ e₄ with
-                   | is_true  h' := is_true (h ▸ h' ▸ rfl)
-                   | is_false h' := is_false (λ he, Expr.no_confusion he (λ h₁ h₂, absurd h₂ h'))
-                   end
+  | is_true h   := (match eq_expr e₂ e₄ with
+                    | is_true  h' := is_true (h ▸ h' ▸ rfl)
+                    | is_false h' := is_false (λ he, Expr.no_confusion he (λ h₁ h₂, absurd h₂ h')))
   | is_false h := is_false (λ he, Expr.no_confusion he (λ h₁ h₂, absurd h₁ h))
-  end
 
 def parse_atom (p : parser Expr) : parser Expr :=
 (Var <$> lexeme var <?> "variable")
diff --git a/tests/lean/run/parser_ir1.lean b/tests/lean/run/parser_ir1.lean
index 7ae61bc66b..43cd5df030 100644
--- a/tests/lean/run/parser_ir1.lean
+++ b/tests/lean/run/parser_ir1.lean
@@ -8,7 +8,6 @@ def show_result {α} [lean.has_to_format α] (p : parser α) (s : string) : io u
 match parse p s with
 | except.ok a    := io.print_ln (lean.to_fmt a)
 | except.error e := io.print_ln (e.to_string s)
-end
 
 def IR := "
 def succ (x : uint32) : uint32 :=
diff --git a/tests/lean/trust0/basic.lean b/tests/lean/trust0/basic.lean
index 1cc2fcd317..37d4772e95 100644
--- a/tests/lean/trust0/basic.lean
+++ b/tests/lean/trust0/basic.lean
@@ -49,7 +49,6 @@ instance : decidable_eq ℕ
     match decidable_eq x y with
     | is_true xeqy := is_true (xeqy ▸ eq.refl (succ x))
     | is_false xney := is_false (λ h, nat.no_confusion h (λ xeqy, absurd xeqy xney))
-    end
 
 def {u} repeat {α : Type u} (f : ℕ → α → α) : ℕ → α → α
 | 0         a := a
@@ -98,7 +97,6 @@ instance decidable_le : ∀ a b : ℕ, decidable (a ≤ b)
   match decidable_le a b with
   | is_true h  := is_true (succ_le_succ h)
   | is_false h := is_false (λ a, h (le_of_succ_le_succ a))
-  end
 
 instance decidable_lt : ∀ a b : ℕ, decidable (a < b) :=
 λ a b, nat.decidable_le (succ a) b