diff --git a/library/algebra/function.lean b/library/algebra/function.lean
index 6caf629e5..d6f6cf11e 100644
--- a/library/algebra/function.lean
+++ b/library/algebra/function.lean
@@ -3,21 +3,19 @@
 -- Author: Leonardo de Moura
 namespace function
 
-section
-  variables {A : Type} {B : Type} {C : Type} {D : Type} {E : Type}
+variables {A : Type} {B : Type} {C : Type} {D : Type} {E : Type}
 
-  definition compose [reducible] (f : B → C) (g : A → B) : A → C :=
-  λx, f (g x)
+definition compose [reducible] (f : B → C) (g : A → B) : A → C :=
+λx, f (g x)
 
-  definition id [reducible] (a : A) : A :=
-  a
+definition id [reducible] (a : A) : A :=
+a
 
-  definition on_fun (f : B → B → C) (g : A → B) : A → A → C :=
-  λx y, f (g x) (g y)
+definition on_fun (f : B → B → C) (g : A → B) : A → A → C :=
+λx y, f (g x) (g y)
 
-  definition combine (f : A → B → C) (op : C → D → E) (g : A → B → D) : A → B → E :=
-  λx y, op (f x y) (g x y)
-end
+definition combine (f : A → B → C) (op : C → D → E) (g : A → B → D) : A → B → E :=
+λx y, op (f x y) (g x y)
 
 definition const {A : Type} (B : Type) (a : A) : B → A :=
 λx, a
diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean
index fe6d75278..49bbe3d2d 100644
--- a/library/data/list/basic.lean
+++ b/library/data/list/basic.lean
@@ -18,7 +18,6 @@ cons   : T → list T → list T
 namespace list
 infix `::` := cons
 
-section
 variable {T : Type}
 
 protected theorem induction_on {P : list T → Prop} (l : list T) (Hnil : P nil)
@@ -258,5 +257,5 @@ nat.rec (λl, head x l) (λm f l, f (tail l)) n l
 theorem nth.zero (x : T) (l : list T) : nth x l 0 = head x l
 
 theorem nth.succ (x : T) (l : list T) (n : nat) : nth x l (succ n) = nth x (tail l) n
-end
+
 end list
diff --git a/library/data/prod.lean b/library/data/prod.lean
index 183bc1459..9994c5a7a 100644
--- a/library/data/prod.lean
+++ b/library/data/prod.lean
@@ -15,12 +15,11 @@ inductive prod (A B : Type) : Type :=
 definition pair := @prod.mk
 
 namespace prod
-infixr `×` := prod
+  infixr `×` := prod
 
--- notation for n-ary tuples
-notation `(` h `,` t:(foldl `,` (e r, prod.mk r e) h) `)` := t
+  -- notation for n-ary tuples
+  notation `(` h `,` t:(foldl `,` (e r, prod.mk r e) h) `)` := t
 
-section
   variables {A B : Type}
   protected theorem destruct {P : A × B → Prop} (p : A × B) (H : ∀a b, P (a, b)) : P p :=
   rec H p
@@ -60,5 +59,4 @@ section
         (assume H, H ▸ and.intro rfl rfl)
         (assume H, and.elim H (assume H₄ H₅, equal H₄ H₅)),
     decidable_iff_equiv _ (iff.symm H₃)
-end
 end prod
diff --git a/library/data/sigma.lean b/library/data/sigma.lean
index e304e4bff..e20d07b64 100644
--- a/library/data/sigma.lean
+++ b/library/data/sigma.lean
@@ -10,7 +10,6 @@ dpair : Πx : A, B x → sigma B
 notation `Σ` binders `,` r:(scoped P, sigma P) := r
 
 namespace sigma
-section
   variables {A : Type} {B : A → Type}
 
   --without reducible tag, slice.composition_functor in algebra.category.constructions fails
@@ -37,10 +36,8 @@ section
   protected definition is_inhabited [instance] (H₁ : inhabited A) (H₂ : inhabited (B (default A))) :
     inhabited (sigma B) :=
   inhabited.destruct H₁ (λa, inhabited.destruct H₂ (λb, inhabited.mk (dpair (default A) b)))
-end
 
-section trip_quad
-  variables {A : Type} {B : A → Type} {C : Πa, B a → Type} {D : Πa b, C a b → Type}
+  variables {C : Πa, B a → Type} {D : Πa b, C a b → Type}
 
   definition dtrip (a : A) (b : B a) (c : C a b) := dpair a (dpair b c)
   definition dquad (a : A) (b : B a) (c : C a b) (d : D a b c) := dpair a (dpair b (dpair c d))
@@ -55,7 +52,6 @@ section trip_quad
       (H₁ : a₁ = a₂)  (H₂ : eq.rec_on H₁ b₁ = b₂) (H₃ : eq.rec_on (congr_arg2_dep C H₁ H₂) c₁ = c₂) :
     dtrip a₁ b₁ c₁ = dtrip a₂ b₂ c₂ :=
   congr_arg3_dep dtrip H₁ H₂ H₃
-end trip_quad
 
   theorem dtrip_eq_ndep {A B : Type} {C : A → B → Type} {a₁ a₂ : A} {b₁ b₂ : B}
       {c₁ : C a₁ b₁} {c₂ : C a₂ b₂} (H₁ : a₁ = a₂)  (H₂ : b₁ = b₂)
diff --git a/library/data/subtype.lean b/library/data/subtype.lean
index bf28ad5af..9f469b5fc 100644
--- a/library/data/subtype.lean
+++ b/library/data/subtype.lean
@@ -12,7 +12,6 @@ inductive subtype {A : Type} (P : A → Prop) : Type :=
 notation `{` binders `,` r:(scoped P, subtype P) `}` := r
 
 namespace subtype
-section
   variables {A : Type} {P : A → Prop}
 
   -- TODO: make this a coercion?
@@ -45,5 +44,4 @@ section
     have H1 : (a1 = a2) ↔ (elt_of a1 = elt_of a2), from
       iff.intro (assume H, eq.subst H rfl) (assume H, equal H),
     decidable_iff_equiv _ (iff.symm H1)
-end
 end subtype
diff --git a/library/data/sum.lean b/library/data/sum.lean
index 5234ef731..44d3189b4 100644
--- a/library/data/sum.lean
+++ b/library/data/sum.lean
@@ -17,7 +17,6 @@ namespace sum
     infixr `+`:25 := sum    -- conflicts with notation for addition
   end extra_notation
 
-  section
   variables {A B : Type}
   variables {a a₁ a₂ : A} {b b₁ b₂ : B}
   protected definition rec_on {C : (A ⊎ B) → Type} (s : A ⊎ B) (H₁ : ∀a : A, C (inl B a)) (H₂ : ∀b : B, C (inr A b)) : C s :=
@@ -83,5 +82,4 @@ namespace sum
             decidable.rec_on (H₂ b₁ b₂)
               (assume Heq : b₁ = b₂, decidable.inl (Heq ▸ rfl))
               (assume Hne : b₁ ≠ b₂, decidable.inr (mt inr_inj Hne))))
-end
 end sum
diff --git a/library/logic/axioms/funext.lean b/library/logic/axioms/funext.lean
index 28070a71c..57b4325b8 100644
--- a/library/logic/axioms/funext.lean
+++ b/library/logic/axioms/funext.lean
@@ -12,8 +12,7 @@ open function
 axiom funext : ∀ {A : Type} {B : A → Type} {f g : Π x, B x} (H : ∀ x, f x = g x), f = g
 
 namespace function
-section
-  parameters {A B C D: Type}
+  variables {A B C D: Type}
 
   theorem compose_assoc (f : C → D) (g : B → C) (h : A → B) : (f ∘ g) ∘ h = f ∘ (g ∘ h) :=
   funext (take x, rfl)
@@ -26,5 +25,4 @@ section
 
   theorem compose_const_right (f : B → C) (b : B) : f ∘ (const A b) = const A (f b) :=
   funext (take x, rfl)
-end
 end function
diff --git a/library/logic/connectives.lean b/library/logic/connectives.lean
index 7a3c03ee0..189e85503 100644
--- a/library/logic/connectives.lean
+++ b/library/logic/connectives.lean
@@ -12,9 +12,9 @@ inductive and (a b : Prop) : Prop :=
 infixr `/\` := and
 infixr `∧` := and
 
+variables {a b c d : Prop}
+
 namespace and
-  section
-  variables {a b c d : Prop}
   theorem elim (H₁ : a ∧ b) (H₂ : a → b → c) : c :=
   rec H₂ H₁
 
@@ -41,7 +41,6 @@ namespace and
 
   theorem imp_right (H₁ : c ∧ a) (H : a → b) : c ∧ b :=
   elim H₁ (assume Hc : c, assume Ha : a, intro Hc (H Ha))
-  end
 end and
 
 -- or
@@ -54,8 +53,6 @@ infixr `\/` := or
 infixr `∨` := or
 
 namespace or
-  section
-  variables {a b c d : Prop}
   theorem inl (Ha : a) : a ∨ b :=
   intro_left b Ha
 
@@ -96,7 +93,6 @@ namespace or
   elim H₁
     (assume H₂ : c, inl H₂)
     (assume H₂ : a, inr (H H₂))
-  end
 end or
 
 theorem not_not_em {p : Prop} : ¬¬(p ∨ ¬p) :=
@@ -113,8 +109,6 @@ infix `<->` := iff
 infix `↔` := iff
 
 namespace iff
-  section
-  variables {a b c : Prop}
   theorem def : (a ↔ b) = ((a → b) ∧ (b → a)) :=
   rfl
 
@@ -158,8 +152,6 @@ namespace iff
 
   theorem false_elim (H : a ↔ false) : ¬a :=
   assume Ha : a, mp H Ha
-
-  end
 end iff
 
 calc_refl iff.refl
@@ -173,8 +165,6 @@ iff.intro (λ Ha, H ▸ Ha) (λ Hb, H⁻¹ ▸ Hb)
 -- comm and assoc for and / or
 -- ---------------------------
 namespace and
-  section
-  variables {a b c : Prop}
   theorem comm : a ∧ b ↔ b ∧ a :=
   iff.intro (λH, swap H) (λH, swap H)
 
@@ -186,12 +176,9 @@ namespace and
     (assume H, intro
       (intro (elim_left H) (elim_left (elim_right H)))
       (elim_right (elim_right H)))
-  end
 end and
 
 namespace or
-  section
-  variables {a b c : Prop}
   theorem comm : a ∨ b ↔ b ∨ a :=
   iff.intro (λH, swap H) (λH, swap H)
 
@@ -207,5 +194,4 @@ namespace or
       (assume H₁, elim H₁
         (assume Hb, inl (inr Hb))
         (assume Hc, inr Hc)))
-  end
 end or
diff --git a/library/logic/decidable.lean b/library/logic/decidable.lean
index ff7f57493..b27bb6b4d 100644
--- a/library/logic/decidable.lean
+++ b/library/logic/decidable.lean
@@ -9,32 +9,30 @@ inl : p  → decidable p,
 inr : ¬p → decidable p
 
 namespace decidable
-
   definition true_decidable [instance] : decidable true :=
   inl trivial
 
   definition false_decidable [instance] : decidable false :=
   inr not_false_trivial
 
-  section
   variables {p q : Prop}
   protected theorem induction_on {C : Prop} (H : decidable p) (H1 : p → C) (H2 : ¬p → C) : C :=
   decidable.rec H1 H2 H
 
-  protected definition rec_on {C : decidable p → Type} (H : decidable p) 
+  protected definition rec_on {C : decidable p → Type} (H : decidable p)
     (H1 : Π(a : p), C (inl a)) (H2 : Π(a : ¬p), C (inr a)) :
     C H :=
   decidable.rec H1 H2 H
 
-  definition rec_on_true {H : decidable p} {H1 : p → Type} {H2 : ¬p → Type} (H3 : p) (H4 : H1 H3) 
+  definition rec_on_true {H : decidable p} {H1 : p → Type} {H2 : ¬p → Type} (H3 : p) (H4 : H1 H3)
       : rec_on H H1 H2 :=
   rec_on H (λh, H4) (λh, false.rec_type _ (h H3))
 
-  definition rec_on_false {H : decidable p} {H1 : p → Type} {H2 : ¬p → Type} (H3 : ¬p) (H4 : H2 H3) 
+  definition rec_on_false {H : decidable p} {H1 : p → Type} {H2 : ¬p → Type} (H3 : ¬p) (H4 : H2 H3)
       : rec_on H H1 H2 :=
   rec_on H (λh, false.rec_type _ (H3 h)) (λh, H4)
 
-  theorem irrelevant [instance] : subsingleton (decidable p) := 
+  theorem irrelevant [instance] : subsingleton (decidable p) :=
   subsingleton.intro (fun d1 d2,
     decidable.rec
       (assume Hp1 : p, decidable.rec
@@ -95,11 +93,9 @@ namespace decidable
   decidable_iff_equiv Hp (eq_to_iff H)
 
   protected theorem rec_subsingleton [instance] {H : decidable p} {H1 : p → Type} {H2 : ¬p → Type}
-      (H3 : Π(h : p), subsingleton (H1 h)) (H4 : Π(h : ¬p), subsingleton (H2 h)) 
+      (H3 : Π(h : p), subsingleton (H1 h)) (H4 : Π(h : ¬p), subsingleton (H2 h))
       : subsingleton (rec_on H H1 H2) :=
   rec_on H (λh, H3 h) (λh, H4 h) --this can be proven using dependent version of "by_cases"
-
-end
 end decidable
 
 definition decidable_rel  {A : Type} (R : A     → Prop) := Π (a   : A), decidable (R a)
diff --git a/library/logic/eq.lean b/library/logic/eq.lean
index 063b9ce26..cdee94207 100644
--- a/library/logic/eq.lean
+++ b/library/logic/eq.lean
@@ -22,7 +22,6 @@ theorem proof_irrel {a : Prop} (H₁ H₂ : a) : H₁ = H₂ :=
 rfl
 
 namespace eq
-section
   variables {A : Type}
   variables {a b c : A}
   theorem id_refl (H₁ : a = a) : H₁ = (eq.refl a) :=
@@ -39,12 +38,12 @@ section
 
   theorem symm (H : a = b) : b = a :=
   subst H (refl a)
-end
-namespace ops
-  postfix `⁻¹` := symm
-  infixr `⬝`   := trans
-  infixr `▸`   := subst
-end ops
+
+  namespace ops
+    postfix `⁻¹` := symm
+    infixr `⬝`   := trans
+    infixr `▸`   := subst
+ end ops
 end eq
 
 calc_subst eq.subst
@@ -205,7 +204,6 @@ definition ne {A : Type} (a b : A) := ¬(a = b)
 infix `≠` := ne
 
 namespace ne
-section
   variable {A : Type}
   variables {a b : A}
 
@@ -220,7 +218,6 @@ section
 
   theorem symm : a ≠ b → b ≠ a :=
   assume (H : a ≠ b) (H₁ : b = a), H (H₁⁻¹)
-end
 end ne
 
 section