diff --git a/library/standard/data/bool.lean b/library/standard/data/bool.lean
index 71dd8e3c7d..6a969a7701 100644
--- a/library/standard/data/bool.lean
+++ b/library/standard/data/bool.lean
@@ -7,8 +7,8 @@ import logic.connectives.basic logic.classes.decidable logic.classes.inhabited
 using eq_ops decidable
 
 inductive bool : Type :=
-| ff : bool
-| tt : bool
+ff : bool,
+tt : bool
 
 namespace bool
 
diff --git a/library/standard/data/list/basic.lean b/library/standard/data/list/basic.lean
index 7a87c4b74e..f65d3608cf 100644
--- a/library/standard/data/list/basic.lean
+++ b/library/standard/data/list/basic.lean
@@ -24,8 +24,8 @@ namespace list
 -- ----
 
 inductive list (T : Type) : Type :=
-| nil {} : list T
-| cons : T → list T → list T
+nil {} : list T,
+cons   : T → list T → list T
 
 infix `::` : 65 := cons
 
diff --git a/library/standard/data/nat/basic.lean b/library/standard/data/nat/basic.lean
index 57d8e36fe0..c411e40eff 100644
--- a/library/standard/data/nat/basic.lean
+++ b/library/standard/data/nat/basic.lean
@@ -25,8 +25,8 @@ using helper_tactics
 
 namespace nat
 inductive nat : Type :=
-| zero : nat
-| succ : nat → nat
+  zero : nat,
+  succ : nat → nat
 
 notation `ℕ`:max := nat
 
diff --git a/library/standard/data/num.lean b/library/standard/data/num.lean
index 4e327f0c32..fb91d77fa9 100644
--- a/library/standard/data/num.lean
+++ b/library/standard/data/num.lean
@@ -12,13 +12,13 @@ namespace num
 -- The parser will generate the terms (pos (bit1 (bit1 (bit0 one)))), zero, and (pos (bit0 (bit1 (bit1 one)))).
 -- This representation can be coerced in whatever we want (e.g., naturals, integers, reals, etc).
 inductive pos_num : Type :=
-| one  : pos_num
-| bit1 : pos_num → pos_num
-| bit0 : pos_num → pos_num
+one  : pos_num,
+bit1 : pos_num → pos_num,
+bit0 : pos_num → pos_num
 
 inductive num : Type :=
-| zero  : num
-| pos   : pos_num → num
+zero  : num,
+pos   : pos_num → num
 
 theorem inhabited_pos_num [instance] : inhabited pos_num :=
 inhabited_mk one
diff --git a/library/standard/data/option.lean b/library/standard/data/option.lean
index a8527a9b67..dec18c439c 100644
--- a/library/standard/data/option.lean
+++ b/library/standard/data/option.lean
@@ -8,14 +8,14 @@ using eq_ops decidable
 namespace option
 
 inductive option (A : Type) : Type :=
-| none {} : option A
-| some    : A → option A
+none {} : option A,
+some    : A → option A
 
-theorem induction_on {A : Type} {p : option A → Prop} (o : option A) 
+theorem induction_on {A : Type} {p : option A → Prop} (o : option A)
   (H1 : p none) (H2 : ∀a, p (some a)) : p o :=
 option_rec H1 H2 o
 
-definition rec_on {A : Type} {C : option A → Type} (o : option A) 
+definition rec_on {A : Type} {C : option A → Type} (o : option A)
   (H1 : C none) (H2 : ∀a, C (some a)) : C o :=
 option_rec H1 H2 o
 
@@ -39,7 +39,7 @@ congr_arg (option_rec a₁ (λ a, a)) H
 theorem option_inhabited [instance] (A : Type) : inhabited (option A) :=
 inhabited_mk none
 
-theorem decidable_eq [instance] {A : Type} {H : ∀a₁ a₂ : A, decidable (a₁ = a₂)} 
+theorem decidable_eq [instance] {A : Type} {H : ∀a₁ a₂ : A, decidable (a₁ = a₂)}
     (o₁ o₂ : option A) : decidable (o₁ = o₂) :=
 rec_on o₁
   (rec_on o₂ (inl (refl _)) (take a₂, (inr (none_ne_some a₂))))
diff --git a/library/standard/data/prod.lean b/library/standard/data/prod.lean
index 9a0e1a319c..688317da80 100644
--- a/library/standard/data/prod.lean
+++ b/library/standard/data/prod.lean
@@ -7,7 +7,7 @@ import logic.classes.inhabited logic.connectives.eq logic.classes.decidable
 using inhabited decidable
 
 inductive prod (A B : Type) : Type :=
-| pair : A → B → prod A B
+pair : A → B → prod A B
 
 precedence `×`:30
 infixr × := prod
@@ -47,8 +47,8 @@ section
       (H2 : decidable (pr2 u = pr2 v)) : decidable (u = v) :=
     have H3 : u = v ↔ (pr1 u = pr1 v) ∧ (pr2 u = pr2 v), from
       iff_intro
-	(assume H, subst H (and_intro (refl _) (refl _)))
-	(assume H, and_elim H (assume H4 H5, prod_eq H4 H5)),
+        (assume H, subst H (and_intro (refl _) (refl _)))
+        (assume H, and_elim H (assume H4 H5, prod_eq H4 H5)),
     decidable_iff_equiv _ (iff_symm H3)
 
 end
diff --git a/library/standard/data/sigma.lean b/library/standard/data/sigma.lean
index 744fa7e3f4..948808c424 100644
--- a/library/standard/data/sigma.lean
+++ b/library/standard/data/sigma.lean
@@ -7,7 +7,7 @@ import logic.classes.inhabited logic.connectives.eq
 using inhabited
 
 inductive sigma {A : Type} (B : A → Type) : Type :=
-| dpair : Πx : A, B x → sigma B
+dpair : Πx : A, B x → sigma B
 
 notation `Σ` binders `,` r:(scoped P, sigma P) := r
 
@@ -36,12 +36,12 @@ section
   (show ∀(b2 : B a2) (H1 : a1 = a2) (H2 : eq_rec_on H1 b1 = b2), dpair a1 b1 = dpair a2 b2, from
     eq_rec
       (take (b2' : B a1),
-	assume (H1' : a1 = a1),
-	assume (H2' : eq_rec_on H1' b1 = b2'),
-	show dpair a1 b1 = dpair a1 b2', from
-	  calc
-	    dpair a1 b1 = dpair a1 (eq_rec_on H1' b1) : {symm (eq_rec_on_id H1' b1)}
-	      ... = dpair a1 b2' : {H2'}) H1)
+        assume (H1' : a1 = a1),
+        assume (H2' : eq_rec_on H1' b1 = b2'),
+        show dpair a1 b1 = dpair a1 b2', from
+          calc
+            dpair a1 b1 = dpair a1 (eq_rec_on H1' b1) : {symm (eq_rec_on_id H1' b1)}
+              ... = dpair a1 b2' : {H2'}) H1)
   b2 H1 H2
 
   theorem sigma_eq {p1 p2 : Σx : A, B x} :
diff --git a/library/standard/data/string.lean b/library/standard/data/string.lean
index 0795fed6a2..464c8521eb 100644
--- a/library/standard/data/string.lean
+++ b/library/standard/data/string.lean
@@ -9,11 +9,11 @@ using bool inhabited
 namespace string
 
 inductive char : Type :=
-| ascii : bool → bool → bool → bool → bool → bool → bool → bool → char
+ascii : bool → bool → bool → bool → bool → bool → bool → bool → char
 
 inductive string : Type :=
-| empty : string
-| str   : char → string → string
+empty : string,
+str   : char → string → string
 
 theorem char_inhabited [instance] : inhabited char :=
 inhabited_mk (ascii ff ff ff ff ff ff ff ff)
diff --git a/library/standard/data/subtype.lean b/library/standard/data/subtype.lean
index c2ab191106..81989f500d 100644
--- a/library/standard/data/subtype.lean
+++ b/library/standard/data/subtype.lean
@@ -7,7 +7,7 @@ import logic.classes.inhabited logic.connectives.eq logic.classes.decidable
 using decidable
 
 inductive subtype {A : Type} (P : A → Prop) : Type :=
-| tag : Πx : A, P x → subtype P
+tag : Πx : A, P x → subtype P
 
 notation `{` binders `|` r:(scoped P, subtype P) `}` := r
 
diff --git a/library/standard/data/sum.lean b/library/standard/data/sum.lean
index 28382b1047..031c3d4f4d 100644
--- a/library/standard/data/sum.lean
+++ b/library/standard/data/sum.lean
@@ -10,8 +10,8 @@ namespace sum
 
 -- TODO: take this outside the namespace when the inductive package handles it better
 inductive sum (A B : Type) : Type :=
-| inl : A → sum A B
-| inr : B → sum A B
+inl : A → sum A B,
+inr : B → sum A B
 
 infixr `+`:25 := sum
 
diff --git a/library/standard/data/unit.lean b/library/standard/data/unit.lean
index 6216d17e43..0860b720a4 100644
--- a/library/standard/data/unit.lean
+++ b/library/standard/data/unit.lean
@@ -9,7 +9,7 @@ using decidable
 namespace unit
 
 inductive unit : Type :=
-| star : unit
+star : unit
 
 notation `⋆`:max := star
 
diff --git a/library/standard/hott/equiv.lean b/library/standard/hott/equiv.lean
index d7cbab5772..4dd3730467 100644
--- a/library/standard/hott/equiv.lean
+++ b/library/standard/hott/equiv.lean
@@ -16,7 +16,7 @@ abbreviation Sect {A B : Type} (s : A → B) (r : B → A) := Πx : A, r (s x) 
 -- Structure IsEquiv
 
 inductive IsEquiv {A B : Type} (f : A → B) :=
-| IsEquiv_mk : Π
+IsEquiv_mk : Π
   (equiv_inv : B → A)
   (eisretr : Sect equiv_inv f)
   (eissect : Sect f equiv_inv)
@@ -40,7 +40,7 @@ IsEquiv_rec (λequiv_inv eisretr eissect eisadj, eisadj) H
 -- Structure Equiv
 
 inductive Equiv (A B : Type) : Type :=
-| Equiv_mk : Π
+Equiv_mk : Π
   (equiv_fun : A → B)
   (equiv_isequiv : IsEquiv equiv_fun),
 Equiv A B
diff --git a/library/standard/hott/fibrant.lean b/library/standard/hott/fibrant.lean
index d58a854cd1..8df3460d9f 100644
--- a/library/standard/hott/fibrant.lean
+++ b/library/standard/hott/fibrant.lean
@@ -8,7 +8,7 @@ import data.prod data.sum data.sigma
 using unit bool nat prod sum sigma
 
 inductive fibrant (T : Type) : Type :=
-| fibrant_mk : fibrant T
+fibrant_mk : fibrant T
 
 namespace fibrant
 
diff --git a/library/standard/hott/path.lean b/library/standard/hott/path.lean
index e21429b8e5..f9ce679d48 100644
--- a/library/standard/hott/path.lean
+++ b/library/standard/hott/path.lean
@@ -6,9 +6,9 @@
 -- TODO: things to test:
 -- o To what extent can we use opaque definitions outside the file?
 -- o Try doing these proofs with tactics.
--- o Try using the simplifier on some of these proofs. 
+-- o Try using the simplifier on some of these proofs.
 
-import general_notation struc.function 
+import general_notation struc.function
 
 using function
 
@@ -16,7 +16,7 @@ using function
 -- ----
 
 inductive path {A : Type} (a : A) : A → Type :=
-| idpath : path a a
+idpath : path a a
 
 infix `≈`:50 := path
 notation x `≈` y:50 `:>`:0 A:0 := @path A x y    -- TODO: is this right?
@@ -58,7 +58,7 @@ definition concat_11 {A : Type} (x : A) : idpath x @ idpath x ≈ idpath x := id
 definition concat_p1 {A : Type} {x y : A} (p : x ≈ y) : p @ idp ≈ p :=
 induction_on p idp
 
--- The identity path is a right unit. 
+-- The identity path is a right unit.
 definition concat_1p {A : Type} {x y : A} (p : x ≈ y) : idp @ p ≈ p :=
 induction_on p idp
 
@@ -111,7 +111,7 @@ induction_on p (induction_on q idp)
 
 -- Inverse is an involution.
 definition inv_V {A : Type} {x y : A} (p : x ≈ y) : p^^ ≈ p :=
-induction_on p idp 
+induction_on p idp
 
 
 -- Theorems for moving things around in equations
@@ -120,7 +120,7 @@ induction_on p idp
 definition moveR_Mp {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) (r : y ≈ x) :
   p ≈ (r^ @ q) → (r @ p) ≈ q :=
 have gen : Πp q, p ≈ (r^ @ q) → (r @ p) ≈ q, from
-  induction_on r 
+  induction_on r
     (take p q,
       assume h : p ≈ idp^ @ q,
       show idp @ p ≈ q, from concat_1p _ @ h @ concat_1p _),
@@ -139,7 +139,7 @@ definition moveR_pV {A : Type} {x y z : A} (p : z ≈ x) (q : y ≈ z) (r : y 
 induction_on p (take q r h, concat_p1 _ @ h @ concat_p1 _) q r
 
 definition moveL_Mp {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) (r : y ≈ x) :
-  r^ @ q ≈ p → q ≈ r @ p := 
+  r^ @ q ≈ p → q ≈ r @ p :=
 induction_on r (take p q h, (concat_1p _)^ @ h @ (concat_1p _)^) p q
 
 definition moveL_pM {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) (r : y ≈ x) :
@@ -231,7 +231,7 @@ calc_refl idpath
 -- More theorems for moving things around in equations
 -- ---------------------------------------------------
 
-definition moveR_transport_p {A : Type} (P : A → Type) {x y : A} (p : x ≈ y) (u : P x) (v : P y) : 
+definition moveR_transport_p {A : Type} (P : A → Type) {x y : A} (p : x ≈ y) (u : P x) (v : P y) :
   u ≈ p^ # v → p # u ≈ v :=
 induction_on p (take u v, id) u v
 
@@ -251,7 +251,7 @@ induction_on p (take u v, id) u v
 -- Functoriality of functions
 -- --------------------------
 
--- Here we prove that functions behave like functors between groupoids, and that [ap] itself is 
+-- Here we prove that functions behave like functors between groupoids, and that [ap] itself is
 -- functorial.
 
 -- Functions take identity paths to identity paths
@@ -290,7 +290,7 @@ induction_on p idp
 
 -- Sometimes we don't have the actual function [compose].
 definition ap_compose' {A B C : Type} (f : A → B) (g : B → C) {x y : A} (p : x ≈ y) :
-  ap (λa, g (f a)) p ≈ ap g (ap f p) := 
+  ap (λa, g (f a)) p ≈ ap g (ap f p) :=
 induction_on p idp
 
 -- The action of constant maps.
@@ -319,18 +319,18 @@ definition concat_pA_pp {A B : Type} {f g : A → B} (p : Πx, f x ≈ g x) {x y
   (r @ ap f q) @ (p y @ s) ≈ (r @ p x) @ (ap g q @ s) :=
 induction_on s (induction_on q idp)
 
-definition concat_pA_p {A B : Type} {f g : A → B} (p : Πx, f x ≈ g x) {x y : A} (q : x ≈ y) 
+definition concat_pA_p {A B : Type} {f g : A → B} (p : Πx, f x ≈ g x) {x y : A} (q : x ≈ y)
     {w : B} (r : w ≈ f x) :
   (r @ ap f q) @ p y ≈ (r @ p x) @ ap g q :=
 induction_on q idp
 
 -- TODO: try this using the simplifier, and compare proofs
-definition concat_A_pp {A B : Type} {f g : A → B} (p : Πx, f x ≈ g x) {x y : A} (q : x ≈ y) 
+definition concat_A_pp {A B : Type} {f g : A → B} (p : Πx, f x ≈ g x) {x y : A} (q : x ≈ y)
     {z : B} (s : g y ≈ z) :
   (ap f q) @ (p y @ s) ≈ (p x) @ (ap g q @ s) :=
-induction_on s (induction_on q 
+induction_on s (induction_on q
   (calc
-    (ap f idp) @ (p x @ idp) ≈ idp @ p x : idp 
+    (ap f idp) @ (p x @ idp) ≈ idp @ p x : idp
       ... ≈ p x : concat_1p _
       ... ≈ (p x) @ (ap g idp @ idp) : idp))
 -- This also works:
@@ -358,7 +358,7 @@ induction_on s (induction_on q (concat_1p _ # idp))
 
 definition concat_pp_A1 {A : Type} {g : A → A} (p : Πx, x ≈ g x) {x y : A} (q : x ≈ y)
     {w : A} (r : w ≈ x) :
-  (r @ p x) @ ap g q ≈ (r @ q) @ p y := 
+  (r @ p x) @ ap g q ≈ (r @ q) @ p y :=
 induction_on q idp
 
 definition concat_p_A1p {A : Type} {g : A → A} (p : Πx, x ≈ g x) {x y : A} (q : x ≈ y)
@@ -378,13 +378,13 @@ definition apD10_pp {A} {B : A → Type} {f f' f'' : Πx, B x} (h : f ≈ f') (h
   apD10 (h @ h') x ≈ apD10 h x @ apD10 h' x :=
 induction_on h (take h', induction_on h' idp) h'
 
-definition apD10_V {A : Type} {B : A → Type} {f g : Πx : A, B x} (h : f ≈ g) (x : A) : 
-  apD10 (h^) x ≈ (apD10 h x)^ := 
+definition apD10_V {A : Type} {B : A → Type} {f g : Πx : A, B x} (h : f ≈ g) (x : A) :
+  apD10 (h^) x ≈ (apD10 h x)^ :=
 induction_on h idp
 
 definition ap10_1 {A B} {f : A → B} (x : A) : ap10 (idpath f) x ≈ idp := idp
 
-definition ap10_pp {A B} {f f' f'' : A → B} (h : f ≈ f') (h' : f' ≈ f'') (x : A) : 
+definition ap10_pp {A B} {f f' f'' : A → B} (h : f ≈ f') (h' : f' ≈ f'') (x : A) :
   ap10 (h @ h') x ≈ ap10 h x @ ap10 h' x := apD10_pp h h' x
 
 definition ap10_V {A B} {f g : A→B} (h : f ≈ g) (x:A) : ap10 (h^) x ≈ (ap10 h x)^ := apD10_V h x
@@ -398,62 +398,62 @@ induction_on p idp
 -- Transport and the groupoid structure of paths
 -- ---------------------------------------------
 
-definition transport_1 {A : Type} (P : A → Type) {x : A} (u : P x) : 
+definition transport_1 {A : Type} (P : A → Type) {x : A} (u : P x) :
   idp # u ≈ u := idp
 
 definition transport_pp {A : Type} (P : A → Type) {x y z : A} (p : x ≈ y) (q : y ≈ z) (u : P x) :
   p @ q # u ≈ q # p # u :=
 induction_on q (induction_on p idp)
 
-definition transport_pV {A : Type} (P : A → Type) {x y : A} (p : x ≈ y) (z : P y) : 
-  p # p^ # z ≈ z := 
+definition transport_pV {A : Type} (P : A → Type) {x y : A} (p : x ≈ y) (z : P y) :
+  p # p^ # z ≈ z :=
 (transport_pp P (p^) p z)^ @ ap (λr, transport P r z) (concat_Vp p)
 
-definition transport_Vp {A : Type} (P : A → Type) {x y : A} (p : x ≈ y) (z : P x) : 
-  p^ # p # z ≈ z := 
+definition transport_Vp {A : Type} (P : A → Type) {x y : A} (p : x ≈ y) (z : P x) :
+  p^ # p # z ≈ z :=
 (transport_pp P p (p^) z)^ @ ap (λr, transport P r z) (concat_pV p)
 
-definition transport_p_pp {A : Type} (P : A → Type) 
-    {x y z w : A} (p : x ≈ y) (q : y ≈ z) (r : z ≈ w) (u : P x) : 
-  ap (λe, e # u) (concat_p_pp p q r) @ (transport_pp P (p @ q) r u) @ 
+definition transport_p_pp {A : Type} (P : A → Type)
+    {x y z w : A} (p : x ≈ y) (q : y ≈ z) (r : z ≈ w) (u : P x) :
+  ap (λe, e # u) (concat_p_pp p q r) @ (transport_pp P (p @ q) r u) @
       ap (transport P r) (transport_pp P p q u)
     ≈ (transport_pp P p (q @ r) u) @ (transport_pp P q r (p # u))
     :> ((p @ (q @ r)) # u ≈ r # q # p # u) :=
 induction_on r (induction_on q (induction_on p idp))
 
 --  Here is another coherence lemma for transport.
-definition transport_pVp {A} (P : A → Type) {x y : A} (p : x ≈ y) (z : P x) : 
-  transport_pV P p (transport P p z) ≈ ap (transport P p) (transport_Vp P p z) := 
+definition transport_pVp {A} (P : A → Type) {x y : A} (p : x ≈ y) (z : P x) :
+  transport_pV P p (transport P p z) ≈ ap (transport P p) (transport_Vp P p z) :=
 induction_on p idp
 
 -- Dependent transport in a doubly dependent type.
 definition transportD {A : Type} (B : A → Type) (C : Π a : A, B a → Type)
-    {x1 x2 : A} (p : x1 ≈ x2) (y : B x1) (z : C x1 y) : 
-  C x2 (p # y) := 
+    {x1 x2 : A} (p : x1 ≈ x2) (y : B x1) (z : C x1 y) :
+  C x2 (p # y) :=
 induction_on p z
 
 -- Transporting along higher-dimensional paths
-definition transport2 {A : Type} (P : A → Type) {x y : A} {p q : x ≈ y} (r : p ≈ q) (z : P x) : 
-  p # z ≈ q # z := 
+definition transport2 {A : Type} (P : A → Type) {x y : A} {p q : x ≈ y} (r : p ≈ q) (z : P x) :
+  p # z ≈ q # z :=
 ap (λp', p' # z) r
 
 -- An alternative definition.
-definition transport2_is_ap10 {A : Type} (Q : A → Type) {x y : A} {p q : x ≈ y} (r : p ≈ q) 
-    (z : Q x) : 
+definition transport2_is_ap10 {A : Type} (Q : A → Type) {x y : A} {p q : x ≈ y} (r : p ≈ q)
+    (z : Q x) :
   transport2 Q r z ≈ ap10 (ap (transport Q) r) z :=
 induction_on r idp
 
 definition transport2_p2p {A : Type} (P : A → Type) {x y : A} {p1 p2 p3 : x ≈ y}
-    (r1 : p1 ≈ p2) (r2 : p2 ≈ p3) (z : P x) : 
+    (r1 : p1 ≈ p2) (r2 : p2 ≈ p3) (z : P x) :
   transport2 P (r1 @ r2) z ≈ transport2 P r1 z @ transport2 P r2 z :=
 induction_on r1 (induction_on r2 idp)
 
-definition transport2_V {A : Type} (Q : A → Type) {x y : A} {p q : x ≈ y} (r : p ≈ q) (z : Q x) : 
+definition transport2_V {A : Type} (Q : A → Type) {x y : A} {p q : x ≈ y} (r : p ≈ q) (z : Q x) :
   transport2 Q (r^) z ≈ ((transport2 Q r z)^) :=
 induction_on r idp
 
-definition concat_AT {A : Type} (P : A → Type) {x y : A} {p q : x ≈ y} {z w : P x} (r : p ≈ q) 
-    (s : z ≈ w) : 
+definition concat_AT {A : Type} (P : A → Type) {x y : A} {p q : x ≈ y} {z w : P x} (r : p ≈ q)
+    (s : z ≈ w) :
   ap (transport P p) s  @  transport2 P r w ≈ transport2 P r z  @  ap (transport P q) s :=
 induction_on r (concat_p1 _ @ (concat_1p _)^)
 
@@ -468,15 +468,15 @@ induction_on p idp
 
 (-- From the Coq HoTT library:
 
-One frequently needs lemmas showing that transport in a certain dependent type is equal to some 
-more explicitly defined operation, defined according to the structure of that dependent type.  
-For most dependent types, we prove these lemmas in the appropriate file in the types/ 
+One frequently needs lemmas showing that transport in a certain dependent type is equal to some
+more explicitly defined operation, defined according to the structure of that dependent type.
+For most dependent types, we prove these lemmas in the appropriate file in the types/
 subdirectory.  Here we consider only the most basic cases.
 
 --)
 
 -- Transporting in a constant fibration.
-definition transport_const {A B : Type} {x1 x2 : A} (p : x1 ≈ x2) (y : B) : 
+definition transport_const {A B : Type} {x1 x2 : A} (p : x1 ≈ x2) (y : B) :
   transport (λx, B) p y ≈ y :=
 induction_on p idp
 
@@ -489,7 +489,7 @@ definition transport_compose {A B} {x y : A} (P : B → Type) (f : A → B) (p :
   transport (λx, P (f x)) p z  ≈  transport P (ap f p) z :=
 induction_on p idp
 
-definition transport_precompose {A B C} (f : A → B) (g g' : B → C) (p : g ≈ g') : 
+definition transport_precompose {A B C} (f : A → B) (g g' : B → C) (p : g ≈ g') :
   transport (λh : B → C, g ∘ f ≈ h ∘ f) p idp ≈ ap (λh, h ∘ f) p :=
 induction_on p idp
 
@@ -497,12 +497,12 @@ definition apD10_ap_precompose {A B C} (f : A → B) (g g' : B → C) (p : g ≈
   apD10 (ap (λh : B → C, h ∘ f) p) a ≈ apD10 p (f a) :=
 induction_on p idp
 
-definition apD10_ap_postcompose {A B C} (f : B → C) (g g' : A → B) (p : g ≈ g') (a : A) : 
+definition apD10_ap_postcompose {A B C} (f : B → C) (g g' : A → B) (p : g ≈ g') (a : A) :
   apD10 (ap (λh : A → B, f ∘ h) p) a ≈ ap f (apD10 p a) :=
 induction_on p idp
 
 -- A special case of [transport_compose] which seems to come up a lot.
-definition transport_idmap_ap A (P : A → Type) x y (p : x ≈ y) (u : P x) : 
+definition transport_idmap_ap A (P : A → Type) x y (p : x ≈ y) (u : P x) :
   transport P p u ≈ transport (λz, z) (ap P p) u :=
 induction_on p idp
 
@@ -520,7 +520,7 @@ induction_on p idp
 -- ------------------------------------
 
 -- Horizontal composition of 2-dimensional paths.
-definition concat2 {A} {x y z : A} {p p' : x ≈ y} {q q' : y ≈ z} (h : p ≈ p') (h' : q ≈ q') : 
+definition concat2 {A} {x y z : A} {p p' : x ≈ y} {q q' : y ≈ z} (h : p ≈ p') (h' : q ≈ q') :
   p @ q ≈ p' @ q' :=
 induction_on h (induction_on h' idp)
 
@@ -534,10 +534,10 @@ induction_on h idp
 -- Whiskering
 -- ----------
 
-definition whiskerL {A : Type} {x y z : A} (p : x ≈ y) {q r : y ≈ z} (h : q ≈ r) : p @ q ≈ p @ r := 
+definition whiskerL {A : Type} {x y z : A} (p : x ≈ y) {q r : y ≈ z} (h : q ≈ r) : p @ q ≈ p @ r :=
 idp @@ h
 
-definition whiskerR {A : Type} {x y z : A} {p q : x ≈ y} (h : p ≈ q) (r : y ≈ z) : p @ r ≈ q @ r := 
+definition whiskerR {A : Type} {x y z : A} {p q : x ≈ y} (h : p ≈ q) (r : y ≈ z) : p @ r ≈ q @ r :=
 h @@ idp
 
 -- Unwhiskering, a.k.a. cancelling
@@ -588,7 +588,7 @@ induction_on b (induction_on a (concat_1p _)^)
 -- Structure corresponding to the coherence equations of a bicategory.
 
 -- The "pentagonator": the 3-cell witnessing the associativity pentagon.
-definition pentagon {A : Type} {v w x y z : A} (p : v ≈ w) (q : w ≈ x) (r : x ≈ y) (s : y ≈ z) : 
+definition pentagon {A : Type} {v w x y z : A} (p : v ≈ w) (q : w ≈ x) (r : x ≈ y) (s : y ≈ z) :
   whiskerL p (concat_p_pp q r s)
     @ concat_p_pp p (q @ r) s
     @ whiskerR (concat_p_pp p q r) s
@@ -596,7 +596,7 @@ definition pentagon {A : Type} {v w x y z : A} (p : v ≈ w) (q : w ≈ x) (r :
 induction_on p (take q, induction_on q (take r, induction_on r (take s, induction_on s idp))) q r s
 
 -- The 3-cell witnessing the left unit triangle.
-definition triangulator {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : 
+definition triangulator {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) :
   concat_p_pp p idp q @ whiskerR (concat_p1 p) q ≈ whiskerL p (concat_1p q) :=
 induction_on p (take q, induction_on q idp) q
 
@@ -614,11 +614,11 @@ definition ap02 {A B : Type} (f:A → B) {x y : A} {p q : x ≈ y} (r : p ≈ q)
 induction_on r idp
 
 definition ap02_pp {A B} (f : A → B) {x y : A} {p p' p'' : x ≈ y} (r : p ≈ p') (r' : p' ≈ p'') :
-  ap02 f (r @ r') ≈ ap02 f r @ ap02 f r' := 
+  ap02 f (r @ r') ≈ ap02 f r @ ap02 f r' :=
 induction_on r (induction_on r' idp)
 
-definition ap02_p2p {A B} (f : A → B) {x y z : A} {p p' : x ≈ y} {q q' :y ≈ z} (r : p ≈ p') 
-    (s : q ≈ q') : 
+definition ap02_p2p {A B} (f : A → B) {x y z : A} {p p' : x ≈ y} {q q' :y ≈ z} (r : p ≈ p')
+    (s : q ≈ q') :
   ap02 f (r @@ s) ≈   ap_pp f p q
                       @ (ap02 f r  @@  ap02 f s)
                       @ (ap_pp f p' q')^ :=
@@ -626,26 +626,26 @@ induction_on r (induction_on s (induction_on q (induction_on p idp)))
 
 -- induction_on r (induction_on s (induction_on p (induction_on q idp)))
 
-definition apD02 {A : Type} {B : A → Type} {x y : A} {p q : x ≈ y} (f : Π x, B x) (r : p ≈ q) : 
+definition apD02 {A : Type} {B : A → Type} {x y : A} {p q : x ≈ y} (f : Π x, B x) (r : p ≈ q) :
   apD f p ≈ transport2 B r (f x) @ apD f q :=
 induction_on r (concat_1p _)^
 
 -- And now for a lemma whose statement is much longer than its proof.
 definition apD02_pp {A} (B : A → Type) (f : Π x:A, B x) {x y : A}
-    {p1 p2 p3 : x ≈ y} (r1 : p1 ≈ p2) (r2 : p2 ≈ p3) : 
+    {p1 p2 p3 : x ≈ y} (r1 : p1 ≈ p2) (r2 : p2 ≈ p3) :
   apD02 f (r1 @ r2) ≈ apD02 f r1
     @ whiskerL (transport2 B r1 (f x)) (apD02 f r2)
     @ concat_p_pp _ _ _
     @ (whiskerR ((transport2_p2p B r1 r2 (f x))^) (apD f p3)) :=
-induction_on r1 (take r2, induction_on r2 (induction_on p1 idp)) r2 
+induction_on r1 (take r2, induction_on r2 (induction_on p1 idp)) r2
 
 
 (-- From the Coq version:
 
 -- ** Tactics, hints, and aliases
 
--- [concat], with arguments flipped. Useful mainly in the idiom [apply (concatR (expression))]. 
--- Given as a notation not a definition so that the resultant terms are literally instances of 
+-- [concat], with arguments flipped. Useful mainly in the idiom [apply (concatR (expression))].
+-- Given as a notation not a definition so that the resultant terms are literally instances of
 -- [concat], with no unfolding required.
 Notation concatR := (λp q, concat q p).
 
diff --git a/library/standard/hott/trunc.lean b/library/standard/hott/trunc.lean
index 3aaecb97a5..f8637a8fbe 100644
--- a/library/standard/hott/trunc.lean
+++ b/library/standard/hott/trunc.lean
@@ -10,7 +10,7 @@ import .path
 -- -----------------
 
 inductive Contr (A : Type) : Type :=
-| Contr_mk : Π
+Contr_mk : Π
   (center : A)
   (contr : Πy : A, center ≈ y),
 Contr A
@@ -21,8 +21,8 @@ definition contr {A : Type} (C : Contr A) : Πy : A, center C ≈ y :=
 Contr_rec (λcenter contr, contr) C
 
 inductive trunc_index : Type :=
-| minus_two : trunc_index
-| trunc_S : trunc_index → trunc_index
+minus_two : trunc_index,
+trunc_S : trunc_index → trunc_index
 
 -- TODO: add coercions to / from nat
 
diff --git a/library/standard/logic/classes/decidable.lean b/library/standard/logic/classes/decidable.lean
index 3a27001597..cc533b2218 100644
--- a/library/standard/logic/classes/decidable.lean
+++ b/library/standard/logic/classes/decidable.lean
@@ -7,8 +7,8 @@ import logic.connectives.basic logic.connectives.eq
 namespace decidable
 
 inductive decidable (p : Prop) : Type :=
-| inl : p  → decidable p
-| inr : ¬p → decidable p
+inl : p  → decidable p,
+inr : ¬p → decidable p
 
 theorem true_decidable [instance] : decidable true :=
 inl trivial
@@ -76,7 +76,7 @@ rec_on Ha
   (assume Hna, rec_on Hb
     (assume Hb  : b,  inr (assume H : a ↔ b, absurd (iff_elim_right H Hb) Hna))
     (assume Hnb : ¬b, inl
-	(iff_intro (assume Ha, absurd_elim b Ha Hna) (assume Hb, absurd_elim a Hb Hnb))))
+        (iff_intro (assume Ha, absurd_elim b Ha Hna) (assume Hb, absurd_elim a Hb Hnb))))
 
 theorem implies_decidable [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) :
   decidable (a → b) :=
diff --git a/library/standard/logic/classes/inhabited.lean b/library/standard/logic/classes/inhabited.lean
index 80e28fff9b..2c8cf3cc55 100644
--- a/library/standard/logic/classes/inhabited.lean
+++ b/library/standard/logic/classes/inhabited.lean
@@ -5,7 +5,7 @@
 import logic.connectives.basic
 
 inductive inhabited (A : Type) : Type :=
-| inhabited_mk : A → inhabited A
+inhabited_mk : A → inhabited A
 
 namespace inhabited
 
diff --git a/library/standard/logic/classes/nonempty.lean b/library/standard/logic/classes/nonempty.lean
index e598374429..9fb8ffe37a 100644
--- a/library/standard/logic/classes/nonempty.lean
+++ b/library/standard/logic/classes/nonempty.lean
@@ -9,7 +9,7 @@ using inhabited
 namespace nonempty
 
 inductive nonempty (A : Type) : Prop :=
-| nonempty_intro : A → nonempty A
+nonempty_intro : A → nonempty A
 
 definition nonempty_elim {A : Type} {B : Type} (H1 : nonempty A) (H2 : A → B) : B :=
 nonempty_rec H2 H1
diff --git a/library/standard/logic/connectives/basic.lean b/library/standard/logic/connectives/basic.lean
index 0fd2ecf287..d8e0831aa2 100644
--- a/library/standard/logic/connectives/basic.lean
+++ b/library/standard/logic/connectives/basic.lean
@@ -19,7 +19,7 @@ theorem false_elim (c : Prop) (H : false) : c :=
 false_rec c H
 
 inductive true : Prop :=
-| trivial : true
+trivial : true
 
 abbreviation not (a : Prop) := a → false
 prefix `¬`:40 := not
@@ -63,7 +63,7 @@ assume Hnb Ha, Hnb (Hab Ha)
 -- ---
 
 inductive and (a b : Prop) : Prop :=
-| and_intro : a → b → and a b
+and_intro : a → b → and a b
 
 infixr `/\`:35 := and
 infixr `∧`:35 := and
@@ -100,8 +100,8 @@ and_elim H1 (assume Hc : c, assume Ha : a, and_intro Hc (H Ha))
 -- --
 
 inductive or (a b : Prop) : Prop :=
-| or_intro_left  : a → or a b
-| or_intro_right : b → or a b
+or_intro_left  : a → or a b,
+or_intro_right : b → or a b
 
 infixr `\/`:30 := or
 infixr `∨`:30 := or
diff --git a/library/standard/logic/connectives/eq.lean b/library/standard/logic/connectives/eq.lean
index 4a67c7f3f5..23d593b211 100644
--- a/library/standard/logic/connectives/eq.lean
+++ b/library/standard/logic/connectives/eq.lean
@@ -10,7 +10,7 @@ import .basic
 -- --
 
 inductive eq {A : Type} (a : A) : A → Prop :=
-| refl : eq a a
+refl : eq a a
 
 infix `=`:50 := eq
 
diff --git a/library/standard/logic/connectives/quantifiers.lean b/library/standard/logic/connectives/quantifiers.lean
index 9eb3a32261..3bb489122d 100644
--- a/library/standard/logic/connectives/quantifiers.lean
+++ b/library/standard/logic/connectives/quantifiers.lean
@@ -7,7 +7,7 @@ import .basic .eq ..classes.nonempty
 using inhabited nonempty
 
 inductive Exists {A : Type} (P : A → Prop) : Prop :=
-| exists_intro : ∀ (a : A), P a → Exists P
+exists_intro : ∀ (a : A), P a → Exists P
 
 notation `exists` binders `,` r:(scoped P, Exists P) := r
 notation `∃` binders `,` r:(scoped P, Exists P) := r
diff --git a/library/standard/struc/relation.lean b/library/standard/struc/relation.lean
index 343693b67d..eed8f0174d 100644
--- a/library/standard/struc/relation.lean
+++ b/library/standard/struc/relation.lean
@@ -16,7 +16,7 @@ abbreviation transitive {T : Type} (R : T → T → Type) : Type := ∀⦃x y z
 
 
 inductive is_reflexive {T : Type} (R : T → T → Type) : Prop :=
-| is_reflexive_mk : reflexive R → is_reflexive R
+is_reflexive_mk : reflexive R → is_reflexive R
 
 namespace is_reflexive
 
@@ -30,7 +30,7 @@ end is_reflexive
 
 
 inductive is_symmetric {T : Type} (R : T → T → Type) : Prop :=
-| is_symmetric_mk : symmetric R → is_symmetric R
+is_symmetric_mk : symmetric R → is_symmetric R
 
 namespace is_symmetric
 
@@ -44,7 +44,7 @@ end is_symmetric
 
 
 inductive is_transitive {T : Type} (R : T → T → Type) : Prop :=
-| is_transitive_mk : transitive R → is_transitive R
+is_transitive_mk : transitive R → is_transitive R
 
 namespace is_transitive
 
@@ -58,7 +58,7 @@ end is_transitive
 
 
 inductive is_equivalence {T : Type} (R : T → T → Type) : Prop :=
-| is_equivalence_mk : is_reflexive R → is_symmetric R → is_transitive R → is_equivalence R
+is_equivalence_mk : is_reflexive R → is_symmetric R → is_transitive R → is_equivalence R
 
 namespace is_equivalence
 
@@ -80,7 +80,7 @@ instance is_equivalence.is_transitive
 
 -- partial equivalence relation
 inductive is_PER {T : Type} (R : T → T → Type) : Prop :=
-| is_PER_mk : is_symmetric R → is_transitive R → is_PER R
+is_PER_mk : is_symmetric R → is_transitive R → is_PER R
 
 namespace is_PER
 
@@ -101,12 +101,12 @@ instance is_PER.is_transitive
 
 inductive congr {T1 : Type} (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop)
     (f : T1 → T2) : Prop :=
-| congr_mk : (∀x y, R1 x y → R2 (f x) (f y)) → congr R1 R2 f
+congr_mk : (∀x y, R1 x y → R2 (f x) (f y)) → congr R1 R2 f
 
 -- for binary functions
 inductive congr2 {T1 : Type}  (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop)
     {T3 : Type} (R3 : T3 → T3 → Prop) (f : T1 → T2 → T3) : Prop :=
-| congr2_mk : (∀(x1 y1 : T1) (x2 y2 : T2), R1 x1 y1 → R2 x2 y2 → R3 (f x1 x2) (f y1 y2)) →
+congr2_mk : (∀(x1 y1 : T1) (x2 y2 : T2), R1 x1 y1 → R2 x2 y2 → R3 (f x1 x2) (f y1 y2)) →
     congr2 R1 R2 R3 f
 
 namespace congr
@@ -171,7 +171,7 @@ congr_mk (λx y H, H)
 -- ---------------------------------------------------------
 
 inductive mp_like {R : Type → Type → Prop} {a b : Type} (H : R a b) : Prop :=
-| mp_like_mk {} : (a → b) → @mp_like R a b H
+mp_like_mk {} : (a → b) → @mp_like R a b H
 
 namespace mp_like
 
diff --git a/library/standard/tools/tactic.lean b/library/standard/tools/tactic.lean
index 74e8de6612..1e3b79e399 100644
--- a/library/standard/tools/tactic.lean
+++ b/library/standard/tools/tactic.lean
@@ -15,7 +15,7 @@ namespace tactic
 -- builtin_tactic is just a "dummy" for creating the
 -- definitions that are actually implemented in C++
 inductive tactic : Type :=
-| builtin_tactic : tactic
+builtin_tactic : tactic
 -- Remark the following names are not arbitrary, the tactic module
 -- uses them when converting Lean expressions into actual tactic objects.
 -- The bultin 'by' construct triggers the process of converting a
diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp
index ece4aa78af..285c736e2b 100644
--- a/src/frontends/lean/inductive_cmd.cpp
+++ b/src/frontends/lean/inductive_cmd.cpp
@@ -27,7 +27,7 @@ namespace lean {
 static name g_assign(":=");
 static name g_with("with");
 static name g_colon(":");
-static name g_bar("|");
+static name g_comma(",");
 static name g_lcurly("{");
 static name g_rcurly("}");
 
@@ -258,8 +258,7 @@ struct inductive_cmd_fn {
     */
     list<intro_rule> parse_intro_rules(buffer<expr> & params) {
         buffer<intro_rule> intros;
-        while (m_p.curr_is_token(g_bar)) {
-            m_p.next();
+        while (true) {
             name intro_name = parse_intro_decl_name();
             bool strict = true;
             if (m_p.curr_is_token(g_lcurly)) {
@@ -273,6 +272,9 @@ struct inductive_cmd_fn {
             intro_type = Pi(params, intro_type, m_p);
             intro_type = infer_implicit(intro_type, params.size(), strict);
             intros.push_back(intro_rule(intro_name, intro_type));
+            if (!m_p.curr_is_token(g_comma))
+                break;
+            m_p.next();
         }
         return to_list(intros.begin(), intros.end());
     }
diff --git a/tests/lean/run/algebra1.lean b/tests/lean/run/algebra1.lean
index 7acfb89d20..b329917e23 100644
--- a/tests/lean/run/algebra1.lean
+++ b/tests/lean/run/algebra1.lean
@@ -17,10 +17,10 @@ end
 
 namespace algebra
   inductive mul_struct (A : Type) : Type :=
-  | mk_mul_struct : (A → A → A) → mul_struct A
+  mk_mul_struct : (A → A → A) → mul_struct A
 
   inductive add_struct (A : Type) : Type :=
-  | mk_add_struct : (A → A → A) → add_struct A
+  mk_add_struct : (A → A → A) → add_struct A
 
   definition mul [inline] {A : Type} {s : mul_struct A} (a b : A)
   := mul_struct_rec (fun f, f) s a b
@@ -35,8 +35,8 @@ end algebra
 
 namespace nat
   inductive nat : Type :=
-  | zero : nat
-  | succ : nat → nat
+  zero : nat,
+  succ : nat → nat
 
   variable add : nat → nat → nat
   variable mul : nat → nat → nat
@@ -55,7 +55,7 @@ end nat
 namespace algebra
 namespace semigroup
   inductive semigroup_struct (A : Type) : Type :=
-  | mk_semigroup_struct : Π (mul : A → A → A), is_assoc mul → semigroup_struct A
+  mk_semigroup_struct : Π (mul : A → A → A), is_assoc mul → semigroup_struct A
 
   definition mul [inline] {A : Type} (s : semigroup_struct A) (a b : A)
   := semigroup_struct_rec (fun f h, f) s a b
@@ -67,7 +67,7 @@ namespace semigroup
   := mk_mul_struct (mul s)
 
   inductive semigroup : Type :=
-  | mk_semigroup : Π (A : Type), semigroup_struct A → semigroup
+  mk_semigroup : Π (A : Type), semigroup_struct A → semigroup
 
   definition carrier [inline] [coercion] (g : semigroup)
   := semigroup_rec (fun c s, c) g
@@ -80,7 +80,7 @@ namespace monoid
   check semigroup.mul
 
   inductive monoid_struct (A : Type) : Type :=
-  | mk_monoid_struct : Π (mul : A → A → A) (id : A), is_assoc mul → is_id mul id → monoid_struct A
+  mk_monoid_struct : Π (mul : A → A → A) (id : A), is_assoc mul → is_id mul id → monoid_struct A
 
   definition mul [inline] {A : Type} (s : monoid_struct A) (a b : A)
   := monoid_struct_rec (fun mul id a i, mul) s a b
@@ -93,7 +93,7 @@ namespace monoid
   := mk_semigroup_struct (mul s) (assoc s)
 
   inductive monoid : Type :=
-  | mk_monoid : Π (A : Type), monoid_struct A → monoid
+  mk_monoid : Π (A : Type), monoid_struct A → monoid
 
   definition carrier [inline] [coercion] (m : monoid)
   := monoid_rec (fun c s, c) m
diff --git a/tests/lean/run/alias3.lean b/tests/lean/run/alias3.lean
index 251d0673d6..48e3d6825d 100644
--- a/tests/lean/run/alias3.lean
+++ b/tests/lean/run/alias3.lean
@@ -17,8 +17,8 @@ namespace N2
   section
     parameter A : Type
     inductive list : Type :=
-    | nil {} : list
-    | cons   : A → list → list
+    nil {} : list,
+    cons   : A → list → list
     check list
   end
   check list
diff --git a/tests/lean/run/class4.lean b/tests/lean/run/class4.lean
index a08ef8b4a7..51fc121486 100644
--- a/tests/lean/run/class4.lean
+++ b/tests/lean/run/class4.lean
@@ -1,8 +1,8 @@
 import standard
 
 inductive nat : Type :=
-| zero : nat
-| succ : nat → nat
+zero : nat,
+succ : nat → nat
 
 definition add (x y : nat)
 := nat_rec x (λ n r, succ r) y
@@ -54,7 +54,7 @@ theorem not_zero_add (x y : nat) (H : ¬ is_zero y) : ¬ is_zero (x + y)
         subst (symm H1) H2)
 
 inductive not_zero (x : nat) : Prop :=
-| not_zero_intro : ¬ is_zero x → not_zero x
+not_zero_intro : ¬ is_zero x → not_zero x
 
 theorem not_zero_not_is_zero {x : nat} (H : not_zero x) : ¬ is_zero x
 := not_zero_rec (λ H1, H1) H
diff --git a/tests/lean/run/class5.lean b/tests/lean/run/class5.lean
index 59b2f08b46..98e1336d44 100644
--- a/tests/lean/run/class5.lean
+++ b/tests/lean/run/class5.lean
@@ -2,7 +2,7 @@ import standard
 
 namespace algebra
   inductive mul_struct (A : Type) : Type :=
-  | mk_mul_struct : (A → A → A) → mul_struct A
+  mk_mul_struct : (A → A → A) → mul_struct A
 
   definition mul [inline] {A : Type} {s : mul_struct A} (a b : A)
   := mul_struct_rec (λ f, f) s a b
@@ -12,8 +12,8 @@ end algebra
 
 namespace nat
   inductive nat : Type :=
-  | zero : nat
-  | succ : nat → nat
+  zero : nat,
+  succ : nat → nat
 
   variable mul : nat → nat → nat
   variable add : nat → nat → nat
diff --git a/tests/lean/run/class6.lean b/tests/lean/run/class6.lean
index c127e2fd15..d72aaaf1e9 100644
--- a/tests/lean/run/class6.lean
+++ b/tests/lean/run/class6.lean
@@ -2,10 +2,10 @@ import standard
 using prod
 
 inductive t1 : Type :=
-| mk1 : t1
+mk1 : t1
 
 inductive t2 : Type :=
-| mk2 : t2
+mk2 : t2
 
 theorem inhabited_t1 : inhabited t1
 := inhabited_mk mk1
@@ -17,4 +17,3 @@ instance inhabited_t1 inhabited_t2
 
 theorem T : inhabited (t1 × t2)
 := _
-
diff --git a/tests/lean/run/class7.lean b/tests/lean/run/class7.lean
index 1538f0de81..c5035fc2a9 100644
--- a/tests/lean/run/class7.lean
+++ b/tests/lean/run/class7.lean
@@ -2,7 +2,7 @@ import standard
 using num tactic
 
 inductive inh (A : Type) : Type :=
-| inh_intro : A -> inh A
+inh_intro : A -> inh A
 
 instance inh_intro
 
diff --git a/tests/lean/run/class8.lean b/tests/lean/run/class8.lean
index 6c99e43828..d38d9205b2 100644
--- a/tests/lean/run/class8.lean
+++ b/tests/lean/run/class8.lean
@@ -2,7 +2,7 @@ import standard
 using num tactic prod
 
 inductive inh (A : Type) : Prop :=
-| inh_intro : A -> inh A
+inh_intro : A -> inh A
 
 instance inh_intro
 
diff --git a/tests/lean/run/class_coe.lean b/tests/lean/run/class_coe.lean
index 16609df54b..0fd7b20589 100644
--- a/tests/lean/run/class_coe.lean
+++ b/tests/lean/run/class_coe.lean
@@ -7,7 +7,7 @@ variable int_add  : int → int → int
 variable real_add : real → real → real
 
 inductive add_struct (A : Type) :=
-| mk : (A → A → A) → add_struct A
+mk : (A → A → A) → add_struct A
 
 definition add {A : Type} {S : add_struct A} (a b : A) : A :=
 add_struct_rec (λ m, m) S a b
@@ -51,4 +51,3 @@ infixl `=`:50 := eq
 abbreviation id (A : Type) (a : A) := a
 notation A `=` B `:` C := @eq C A B
 check nat_to_int n + nat_to_int m = (n + m) : int
-
diff --git a/tests/lean/run/coe1.lean b/tests/lean/run/coe1.lean
index 948b9d23cf..01f106c8e7 100644
--- a/tests/lean/run/coe1.lean
+++ b/tests/lean/run/coe1.lean
@@ -18,7 +18,7 @@ set_option pp.universes true
 check eq a1 b1
 
 inductive pair (A : Type) (B: Type) : Type :=
-| mk_pair : A → B → pair A B
+mk_pair : A → B → pair A B
 
 check mk_pair a1 b2
 check B
diff --git a/tests/lean/run/coe2.lean b/tests/lean/run/coe2.lean
index 13e87d72ba..4232158dda 100644
--- a/tests/lean/run/coe2.lean
+++ b/tests/lean/run/coe2.lean
@@ -2,7 +2,7 @@ import standard
 
 namespace setoid
   inductive setoid : Type :=
-  | mk_setoid: Π (A : Type), (A → A → Prop) → setoid
+  mk_setoid: Π (A : Type), (A → A → Prop) → setoid
 
   definition carrier (s : setoid)
   := setoid_rec (λ a eq, a) s
@@ -15,6 +15,6 @@ namespace setoid
   coercion carrier
 
   inductive morphism (s1 s2 : setoid) : Type :=
-  | mk_morphism : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism s1 s2
+  mk_morphism : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism s1 s2
 
 end setoid
\ No newline at end of file
diff --git a/tests/lean/run/coe3.lean b/tests/lean/run/coe3.lean
index d820c102af..8b389ef520 100644
--- a/tests/lean/run/coe3.lean
+++ b/tests/lean/run/coe3.lean
@@ -2,7 +2,7 @@ import standard
 
 namespace setoid
   inductive setoid : Type :=
-  | mk_setoid: Π (A : Type), (A → A → Prop) → setoid
+  mk_setoid: Π (A : Type), (A → A → Prop) → setoid
 
   definition carrier (s : setoid)
   := setoid_rec (λ a eq, a) s
@@ -15,7 +15,7 @@ namespace setoid
   coercion carrier
 
   inductive morphism (s1 s2 : setoid) : Type :=
-  | mk_morphism : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism s1 s2
+  mk_morphism : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism s1 s2
 
   set_option pp.universes true
 
@@ -24,7 +24,7 @@ namespace setoid
   check λ (s1 s2 : Type), s1
 
   inductive morphism2 (s1 : setoid) (s2 : setoid) : Type :=
-  | mk_morphism2 : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism2 s1 s2
+  mk_morphism2 : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism2 s1 s2
 
   check mk_morphism2
 end setoid
\ No newline at end of file
diff --git a/tests/lean/run/coe4.lean b/tests/lean/run/coe4.lean
index ffbbaf56f7..93d754dfa5 100644
--- a/tests/lean/run/coe4.lean
+++ b/tests/lean/run/coe4.lean
@@ -2,7 +2,7 @@ import standard
 
 namespace setoid
   inductive setoid : Type :=
-  | mk_setoid: Π (A : Type'), (A → A → Prop) → setoid
+  mk_setoid: Π (A : Type'), (A → A → Prop) → setoid
 
   set_option pp.universes true
 
@@ -20,14 +20,14 @@ namespace setoid
   coercion carrier
 
   inductive morphism (s1 s2 : setoid) : Type :=
-  | mk_morphism : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism s1 s2
+  mk_morphism : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism s1 s2
 
   check mk_morphism
   check λ (s1 s2 : setoid), s1
   check λ (s1 s2 : Type), s1
 
   inductive morphism2 (s1 : setoid) (s2 : setoid) : Type :=
-  | mk_morphism2 : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism2 s1 s2
+  mk_morphism2 : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism2 s1 s2
 
   check morphism2
   check mk_morphism2
diff --git a/tests/lean/run/coe5.lean b/tests/lean/run/coe5.lean
index ab0a5d3b47..29632118b6 100644
--- a/tests/lean/run/coe5.lean
+++ b/tests/lean/run/coe5.lean
@@ -2,7 +2,7 @@ import standard
 
 namespace setoid
   inductive setoid : Type :=
-  | mk_setoid: Π (A : Type'), (A → A → Prop) → setoid
+  mk_setoid: Π (A : Type'), (A → A → Prop) → setoid
 
   set_option pp.universes true
 
@@ -20,20 +20,20 @@ namespace setoid
   coercion carrier
 
   inductive morphism (s1 s2 : setoid) : Type :=
-  | mk_morphism : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism s1 s2
+  mk_morphism : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism s1 s2
 
   check mk_morphism
   check λ (s1 s2 : setoid), s1
   check λ (s1 s2 : Type), s1
 
   inductive morphism2 (s1 : setoid) (s2 : setoid) : Type :=
-  | mk_morphism2 : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism2 s1 s2
+  mk_morphism2 : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism2 s1 s2
 
   check morphism2
   check mk_morphism2
 
   inductive my_struct : Type :=
-  | mk_foo : Π (s1 s2 : setoid) (s3 s4 : setoid), morphism2 s1 s2 → morphism2 s3 s4 → my_struct
+  mk_foo : Π (s1 s2 : setoid) (s3 s4 : setoid), morphism2 s1 s2 → morphism2 s3 s4 → my_struct
 
   check my_struct
   definition tst2 : Type.{4} := my_struct.{1 2 1 2}
diff --git a/tests/lean/run/coercion_bug2.lean b/tests/lean/run/coercion_bug2.lean
index d94365412b..ff61c01862 100644
--- a/tests/lean/run/coercion_bug2.lean
+++ b/tests/lean/run/coercion_bug2.lean
@@ -2,10 +2,9 @@ import data.nat
 using nat
 
 inductive list (T : Type) : Type :=
-| nil {} : list T
-| cons : T → list T → list T
+nil {} : list T,
+cons : T → list T → list T
 
 definition length {T : Type} : list T → nat := list_rec 0 (fun x l m, succ m)
 theorem length_nil {T : Type} : length (@nil T) = 0
 := refl _
-
diff --git a/tests/lean/run/congr_imp_bug.lean b/tests/lean/run/congr_imp_bug.lean
index ab0c2f6e3e..fb4d5dbc82 100644
--- a/tests/lean/run/congr_imp_bug.lean
+++ b/tests/lean/run/congr_imp_bug.lean
@@ -10,7 +10,7 @@ namespace congr
 
 inductive struc {T1 : Type} {T2 : Type} (R1 : T1 → T1 → Prop) (R2 : T2 → T2 → Prop)
     (f : T1 → T2) : Prop :=
-| mk : (∀x y : T1, R1 x y → R2 (f x) (f y)) → struc R1 R2 f
+mk : (∀x y : T1, R1 x y → R2 (f x) (f y)) → struc R1 R2 f
 
 abbreviation app {T1 : Type} {T2 : Type} {R1 : T1 → T1 → Prop} {R2 : T2 → T2 → Prop}
     {f : T1 → T2} (C : struc R1 R2 f) {x y : T1} : R1 x y → R2 (f x) (f y) :=
@@ -18,7 +18,7 @@ struc_rec id C x y
 
 inductive struc2 {T1 : Type} {T2 : Type} {T3 : Type} (R1 : T1 → T1 → Prop)
     (R2 : T2 → T2 → Prop) (R3 : T3 → T3 → Prop) (f : T1 → T2 → T3) : Prop :=
-| mk2 : (∀(x1 y1 : T1) (x2 y2 : T2), R1 x1 y1 → R2 x2 y2 → R3 (f x1 x2) (f y1 y2)) →
+mk2 : (∀(x1 y1 : T1) (x2 y2 : T2), R1 x1 y1 → R2 x2 y2 → R3 (f x1 x2) (f y1 y2)) →
     struc2 R1 R2 R3 f
 
 abbreviation app2 {T1 : Type} {T2 : Type} {T3 : Type} {R1 : T1 → T1 → Prop}
diff --git a/tests/lean/run/e14.lean b/tests/lean/run/e14.lean
index 40bc507856..d4e22922f8 100644
--- a/tests/lean/run/e14.lean
+++ b/tests/lean/run/e14.lean
@@ -1,10 +1,10 @@
 inductive nat : Type :=
-| zero : nat
-| succ : nat → nat
+zero : nat,
+succ : nat → nat
 
 inductive list (A : Type) : Type :=
-| nil {} : list A
-| cons   : A → list A → list A
+nil {} : list A,
+cons   : A → list A → list A
 
 check nil
 check nil.{1}
@@ -14,8 +14,8 @@ check @nil nat
 check cons zero nil
 
 inductive vector (A : Type) : nat → Type :=
-| vnil {} : vector A zero
-| vcons   : forall {n : nat}, A → vector A n → vector A (succ n)
+vnil {} : vector A zero,
+vcons   : forall {n : nat}, A → vector A n → vector A (succ n)
 
 check vcons zero vnil
 variable n : nat
diff --git a/tests/lean/run/e15.lean b/tests/lean/run/e15.lean
index 1bcac11f15..e31ef27f55 100644
--- a/tests/lean/run/e15.lean
+++ b/tests/lean/run/e15.lean
@@ -1,10 +1,10 @@
 inductive nat : Type :=
-| zero : nat
-| succ : nat → nat
+zero : nat,
+succ : nat → nat
 
 inductive list (A : Type) : Type :=
-| nil {} : list A
-| cons   : A → list A → list A
+nil {} : list A,
+cons   : A → list A → list A
 
 check nil
 check nil.{1}
@@ -14,8 +14,8 @@ check @nil nat
 check cons zero nil
 
 inductive vector (A : Type) : nat → Type :=
-| vnil {} : vector A zero
-| vcons   : forall {n : nat}, A → vector A n → vector A (succ n)
+vnil {} : vector A zero,
+vcons   : forall {n : nat}, A → vector A n → vector A (succ n)
 
 check vcons zero vnil
 variable n : nat
diff --git a/tests/lean/run/e16.lean b/tests/lean/run/e16.lean
index 2484963ec6..00e1e5bbd2 100644
--- a/tests/lean/run/e16.lean
+++ b/tests/lean/run/e16.lean
@@ -1,10 +1,10 @@
 inductive nat : Type :=
-| zero : nat
-| succ : nat → nat
+zero : nat,
+succ : nat → nat
 
 inductive list (A : Type) : Type :=
-| nil {} : list A
-| cons   : A → list A → list A
+nil {} : list A,
+cons   : A → list A → list A
 
 check nil
 check nil.{1}
@@ -14,8 +14,8 @@ check @nil nat
 check cons zero nil
 
 inductive vector (A : Type) : nat → Type :=
-| vnil {} : vector A zero
-| vcons   : forall {n : nat}, A → vector A n → vector A (succ n)
+vnil {} : vector A zero,
+vcons   : forall {n : nat}, A → vector A n → vector A (succ n)
 
 check vcons zero vnil
 variable n : nat
diff --git a/tests/lean/run/e17.lean b/tests/lean/run/e17.lean
index 849db414bf..67745fe966 100644
--- a/tests/lean/run/e17.lean
+++ b/tests/lean/run/e17.lean
@@ -1,14 +1,14 @@
 inductive nat : Type :=
-| zero : nat
-| succ : nat → nat
+zero : nat,
+succ : nat → nat
 
 inductive list (A : Type) : Type :=
-| nil {} : list A
-| cons   : A → list A → list A
+nil {} : list A,
+cons   : A → list A → list A
 
 inductive int : Type :=
-| of_nat : nat → int
-| neg : nat → int
+of_nat : nat → int,
+neg : nat → int
 
 coercion of_nat
 
diff --git a/tests/lean/run/e18.lean b/tests/lean/run/e18.lean
index 400bc1362c..9aa3dcdba8 100644
--- a/tests/lean/run/e18.lean
+++ b/tests/lean/run/e18.lean
@@ -1,14 +1,14 @@
 inductive nat : Type :=
-| zero : nat
-| succ : nat → nat
+zero : nat,
+succ : nat → nat
 
 inductive list (A : Type) : Type :=
-| nil {} : list A
-| cons   : A → list A → list A
+nil {} : list A,
+cons   : A → list A → list A
 
 inductive int : Type :=
-| of_nat : nat → int
-| neg : nat → int
+of_nat : nat → int,
+neg : nat → int
 
 coercion of_nat
 
diff --git a/tests/lean/run/e5.lean b/tests/lean/run/e5.lean
index 393a870154..a9c3635eac 100644
--- a/tests/lean/run/e5.lean
+++ b/tests/lean/run/e5.lean
@@ -32,8 +32,8 @@ theorem trans {A : Type} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c
 := subst H2 H1
 
 inductive nat : Type :=
-| zero : nat
-| succ : nat → nat
+zero : nat,
+succ : nat → nat
 
 print "using strict implicit arguments"
 abbreviation symmetric {A : Type} (R : A → A → Prop) := ∀ ⦃a b⦄, R a b → R b a
@@ -66,4 +66,3 @@ axiom H5 : symmetric3 p
 axiom H6 : p zero (succ zero)
 check H5
 check H5 H6
-
diff --git a/tests/lean/run/elab_bug1.lean b/tests/lean/run/elab_bug1.lean
index 8604345557..66a529af79 100644
--- a/tests/lean/run/elab_bug1.lean
+++ b/tests/lean/run/elab_bug1.lean
@@ -18,7 +18,7 @@ abbreviation reflexive {T : Type} (R : T → T → Type) : Prop := ∀x, R x x
 
 inductive congruence {T1 : Type} {T2 : Type} (R1 : T1 → T1 → Prop) (R2 : T2 → T2 → Prop)
     (f : T1 → T2) : Prop :=
-| mk : (∀x y : T1, R1 x y → R2 (f x) (f y)) → congruence R1 R2 f
+mk : (∀x y : T1, R1 x y → R2 (f x) (f y)) → congruence R1 R2 f
 
 -- to trigger class inference
 theorem congr_app {T1 : Type} {T2 : Type} (R1 : T1 → T1 → Prop) (R2 : T2 → T2 → Prop)
diff --git a/tests/lean/run/group.lean b/tests/lean/run/group.lean
index 5a19380f5e..19b8a523b6 100644
--- a/tests/lean/run/group.lean
+++ b/tests/lean/run/group.lean
@@ -14,10 +14,10 @@ section
 end
 
 inductive group_struct (A : Type) : Type :=
-| mk_group_struct : Π (mul : A → A → A) (one : A) (inv : A → A), is_assoc mul → is_id mul one → is_inv mul one inv → group_struct A
+mk_group_struct : Π (mul : A → A → A) (one : A) (inv : A → A), is_assoc mul → is_id mul one → is_inv mul one inv → group_struct A
 
 inductive group : Type :=
-| mk_group : Π (A : Type), group_struct A → group
+mk_group : Π (A : Type), group_struct A → group
 
 definition carrier (g : group) : Type
 := group_rec (λ c s, c) g
diff --git a/tests/lean/run/group2.lean b/tests/lean/run/group2.lean
index 5d1b2b6f23..97fe37a799 100644
--- a/tests/lean/run/group2.lean
+++ b/tests/lean/run/group2.lean
@@ -14,10 +14,10 @@ section
 end
 
 inductive group_struct (A : Type) : Type :=
-| mk_group_struct : Π (mul : A → A → A) (one : A) (inv : A → A), is_assoc mul → is_id mul one → is_inv mul one inv → group_struct A
+mk_group_struct : Π (mul : A → A → A) (one : A) (inv : A → A), is_assoc mul → is_id mul one → is_inv mul one inv → group_struct A
 
 inductive group : Type :=
-| mk_group : Π (A : Type), group_struct A → group
+mk_group : Π (A : Type), group_struct A → group
 
 definition carrier (g : group) : Type
 := group_rec (λ c s, c) g
diff --git a/tests/lean/run/ind0.lean b/tests/lean/run/ind0.lean
index 7730dcf30d..95d5c81c3d 100644
--- a/tests/lean/run/ind0.lean
+++ b/tests/lean/run/ind0.lean
@@ -1,6 +1,6 @@
 inductive nat : Type :=
-| zero : nat
-| succ : nat → nat
+zero : nat,
+succ : nat → nat
 
 check nat
 check nat_rec.{1}
\ No newline at end of file
diff --git a/tests/lean/run/ind1.lean b/tests/lean/run/ind1.lean
index 47d236b39f..b67940d6ed 100644
--- a/tests/lean/run/ind1.lean
+++ b/tests/lean/run/ind1.lean
@@ -1,6 +1,6 @@
 inductive list (A : Type) : Type :=
-| nil  : list A
-| cons : A → list A → list A
+nil  : list A,
+cons : A → list A → list A
 
 check list.{1}
 check cons.{1}
diff --git a/tests/lean/run/ind2.lean b/tests/lean/run/ind2.lean
index 92aa21308b..927f671735 100644
--- a/tests/lean/run/ind2.lean
+++ b/tests/lean/run/ind2.lean
@@ -1,10 +1,10 @@
 inductive nat : Type :=
-| zero : nat
-| succ : nat → nat
+zero : nat,
+succ : nat → nat
 
 inductive vector (A : Type) : nat → Type :=
-| vnil  : vector A zero
-| vcons : Π {n : nat}, A → vector A n → vector A (succ n)
+vnil  : vector A zero,
+vcons : Π {n : nat}, A → vector A n → vector A (succ n)
 
 check vector.{1}
 check vnil.{1}
diff --git a/tests/lean/run/ind3.lean b/tests/lean/run/ind3.lean
index 27cc3c794e..d2234b2fc9 100644
--- a/tests/lean/run/ind3.lean
+++ b/tests/lean/run/ind3.lean
@@ -1,8 +1,8 @@
 inductive tree (A : Type) : Type :=
-| node : A → forest A → tree A
+node : A → forest A → tree A
 with forest (A : Type) : Type :=
-| nil  : forest A
-| cons : tree A → forest A → forest A
+nil  : forest A,
+cons : tree A → forest A → forest A
 
 check tree.{1}
 check forest.{1}
@@ -12,7 +12,7 @@ check forest_rec.{1 1}
 print "==============="
 
 inductive group : Type :=
-| mk_group : Π (carrier : Type) (mul : carrier → carrier → carrier) (one : carrier), group
+mk_group : Π (carrier : Type) (mul : carrier → carrier → carrier) (one : carrier), group
 
 check group.{1}
 check group.{2}
diff --git a/tests/lean/run/ind4.lean b/tests/lean/run/ind4.lean
index 3c6009143b..fde14a2d38 100644
--- a/tests/lean/run/ind4.lean
+++ b/tests/lean/run/ind4.lean
@@ -1,8 +1,8 @@
 section
   parameter A : Type
   inductive list : Type :=
-  | nil  : list
-  | cons : A → list → list
+  nil  : list,
+  cons : A → list → list
 end
 
 check list.{1}
@@ -11,10 +11,10 @@ check cons.{1}
 section
   parameter A : Type
   inductive tree : Type :=
-  | node : A → forest → tree
+  node : A → forest → tree
   with forest : Type :=
-  | fnil  : forest
-  | fcons : tree → forest → forest
+  fnil  : forest,
+  fcons : tree → forest → forest
   check tree
   check forest
 end
diff --git a/tests/lean/run/ind5.lean b/tests/lean/run/ind5.lean
index 77a65d18bd..57e3962d86 100644
--- a/tests/lean/run/ind5.lean
+++ b/tests/lean/run/ind5.lean
@@ -1,8 +1,8 @@
 definition Prop [inline] : Type.{1} := Type.{0}
 
 inductive or (A B : Prop) : Prop :=
-| or_intro_left  : A → or A B
-| or_intro_right : B → or A B
+or_intro_left  : A → or A B,
+or_intro_right : B → or A B
 
 check or
 check or_intro_left
diff --git a/tests/lean/run/ind6.lean b/tests/lean/run/ind6.lean
index 611dfc7cbe..95eec64af3 100644
--- a/tests/lean/run/ind6.lean
+++ b/tests/lean/run/ind6.lean
@@ -1,8 +1,8 @@
 inductive tree.{u} (A : Type.{u}) : Type.{max u 1} :=
-| node : A → forest.{u} A → tree.{u} A
+node : A → forest.{u} A → tree.{u} A
 with forest.{u} (A : Type.{u}) : Type.{max u 1} :=
-| nil  : forest.{u} A
-| cons : tree.{u} A → forest.{u} A → forest.{u} A
+nil  : forest.{u} A,
+cons : tree.{u} A → forest.{u} A → forest.{u} A
 
 check tree.{1}
 check forest.{1}
diff --git a/tests/lean/run/ind7.lean b/tests/lean/run/ind7.lean
index dbbca13976..8110d609ea 100644
--- a/tests/lean/run/ind7.lean
+++ b/tests/lean/run/ind7.lean
@@ -1,7 +1,7 @@
 namespace list
   inductive list (A : Type) : Type :=
-  | nil  : list A
-  | cons : A → list A → list A
+  nil  : list A,
+  cons : A → list A → list A
 
   check list.{1}
   check cons.{1}
diff --git a/tests/lean/run/indimp.lean b/tests/lean/run/indimp.lean
index bb3a24499e..1a5c5c0397 100644
--- a/tests/lean/run/indimp.lean
+++ b/tests/lean/run/indimp.lean
@@ -1,21 +1,19 @@
 abbreviation Prop := Type.{0}
 
 inductive nat :=
-| zero : nat
-| succ : nat → nat
+zero : nat,
+succ : nat → nat
 
 inductive list (A : Type) :=
-| nil {} : list A
-| cons   : A → list A → list A
+nil {} : list A,
+cons   : A → list A → list A
 
 inductive list2 (A : Type) : Type :=
-| nil2 {} : list2 A
-| cons2   : A → list2 A → list2 A
+nil2 {} : list2 A,
+cons2   : A → list2 A → list2 A
 
 inductive and (A B : Prop) : Prop :=
-| and_intro : A → B → and A B
+and_intro : A → B → and A B
 
 inductive class {T1 : Type} (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop) (f : T1 → T2) :=
-| mk : (∀x y : T1, R1 x y → R2 (f x) (f y)) → class R1 R2 f
-
-
+mk : (∀x y : T1, R1 x y → R2 (f x) (f y)) → class R1 R2 f
diff --git a/tests/lean/run/induniv.lean b/tests/lean/run/induniv.lean
index 8aa86fc27d..6b3fc73b43 100644
--- a/tests/lean/run/induniv.lean
+++ b/tests/lean/run/induniv.lean
@@ -1,45 +1,45 @@
 inductive list (A : Type) : Type :=
-| nil {} : list A
-| cons   : A → list A → list A
+nil {} : list A,
+cons   : A → list A → list A
 
 section
   parameter A : Type
   inductive list2 : Type :=
-  | nil2 {} : list2
-  | cons2   : A → list2 → list2
+  nil2 {} : list2,
+  cons2   : A → list2 → list2
 end
 
 variable num : Type.{1}
 
 namespace Tree
 inductive tree (A : Type) : Type :=
-| node : A → forest A → tree A
+node : A → forest A → tree A
 with forest (A : Type) : Type :=
-| nil  : forest A
-| cons : tree A → forest A → forest A
+nil  : forest A,
+cons : tree A → forest A → forest A
 end Tree
 
 inductive group_struct (A : Type) : Type :=
-| mk_group_struct : (A → A → A) → A → group_struct A
+mk_group_struct : (A → A → A) → A → group_struct A
 
 inductive group : Type :=
-| mk_group : Π (A : Type), (A → A → A) → A → group
+mk_group : Π (A : Type), (A → A → A) → A → group
 
 section
   parameter A : Type
   parameter B : Type
   inductive pair : Type :=
-  | mk_pair : A → B → pair
+  mk_pair : A → B → pair
 end
 
 definition Prop [inline] := Type.{0}
 inductive eq {A : Type} (a : A) : A → Prop :=
-| refl : eq a a
+refl : eq a a
 
 section
   parameter {A : Type}
   inductive eq2 (a : A) : A → Prop :=
-  | refl2 : eq2 a a
+  refl2 : eq2 a a
 end
 
 
@@ -47,5 +47,5 @@ section
   parameter A : Type
   parameter B : Type
   inductive triple (C : Type) : Type :=
-  | mk_triple : A → B → C → triple C
+  mk_triple : A → B → C → triple C
 end
diff --git a/tests/lean/run/is_nil.lean b/tests/lean/run/is_nil.lean
index cc8df82cda..15315a2a27 100644
--- a/tests/lean/run/is_nil.lean
+++ b/tests/lean/run/is_nil.lean
@@ -2,8 +2,8 @@ import standard
 using tactic
 
 inductive list (A : Type) : Type :=
-| nil {} : list A
-| cons   : A → list A → list A
+nil {} : list A,
+cons   : A → list A → list A
 
 definition is_nil {A : Type} (l : list A) : Prop
 := list_rec true (fun h t r, false) l
diff --git a/tests/lean/run/list_elab1.lean b/tests/lean/run/list_elab1.lean
index 7de3d84c7e..47f71cd8b3 100644
--- a/tests/lean/run/list_elab1.lean
+++ b/tests/lean/run/list_elab1.lean
@@ -12,8 +12,8 @@
 import data.nat
 using nat eq_ops
 inductive list (T : Type) : Type :=
-| nil {} : list T
-| cons : T → list T → list T
+nil {} : list T,
+cons : T → list T → list T
 
 theorem list_induction_on {T : Type} {P : list T → Prop} (l : list T) (Hnil : P nil)
     (Hind : forall x : T, forall l : list T, forall H : P l, P (cons x l)) : P l :=
diff --git a/tests/lean/run/nat_bug.lean b/tests/lean/run/nat_bug.lean
index 6c65401b17..ba055e69c4 100644
--- a/tests/lean/run/nat_bug.lean
+++ b/tests/lean/run/nat_bug.lean
@@ -2,8 +2,8 @@ import logic
 using decidable
 
 inductive nat : Type :=
-| zero : nat
-| succ : nat → nat
+zero : nat,
+succ : nat → nat
 
 theorem induction_on {P : nat → Prop} (a : nat) (H1 : P zero) (H2 : ∀ (n : nat) (IH : P n), P (succ n)) : P a
 := nat_rec H1 H2 a
diff --git a/tests/lean/run/nat_bug2.lean b/tests/lean/run/nat_bug2.lean
index 41b0c50f99..8cf733910c 100644
--- a/tests/lean/run/nat_bug2.lean
+++ b/tests/lean/run/nat_bug2.lean
@@ -2,8 +2,8 @@ import standard
 using num eq_ops
 
 inductive nat : Type :=
-| zero : nat
-| succ : nat → nat
+zero : nat,
+succ : nat → nat
 
 abbreviation plus (x y : nat) : nat
 := nat_rec x (λn r, succ r) y
diff --git a/tests/lean/run/nat_bug3.lean b/tests/lean/run/nat_bug3.lean
index c2ae2b4749..67af5214b9 100644
--- a/tests/lean/run/nat_bug3.lean
+++ b/tests/lean/run/nat_bug3.lean
@@ -2,8 +2,8 @@ import standard
 using num eq_ops
 
 inductive nat : Type :=
-| zero : nat
-| succ : nat → nat
+zero : nat,
+succ : nat → nat
 
 abbreviation plus (x y : nat) : nat
 := nat_rec x (λn r, succ r) y
diff --git a/tests/lean/run/nat_bug4.lean b/tests/lean/run/nat_bug4.lean
index d90c5b4824..7e3c1eb1c4 100644
--- a/tests/lean/run/nat_bug4.lean
+++ b/tests/lean/run/nat_bug4.lean
@@ -2,8 +2,8 @@ import standard
 using num eq_ops
 
 inductive nat : Type :=
-| zero : nat
-| succ : nat → nat
+zero : nat,
+succ : nat → nat
 
 definition add (x y : nat) : nat := nat_rec x (λn r, succ r) y
 infixl `+`:65 := add
@@ -14,4 +14,3 @@ axiom mul_succ_right (n m : nat) : n * succ m = n * m + n
 
 theorem small2 (n m l : nat) : n * succ l + m = n * l + n + m
 := subst (mul_succ_right _ _) (refl (n * succ l + m))
-
diff --git a/tests/lean/run/nat_bug5.lean b/tests/lean/run/nat_bug5.lean
index c50220a81c..d863a9f207 100644
--- a/tests/lean/run/nat_bug5.lean
+++ b/tests/lean/run/nat_bug5.lean
@@ -2,8 +2,8 @@ import standard
 using num eq_ops
 
 inductive nat : Type :=
-| zero : nat
-| succ : nat → nat
+zero : nat,
+succ : nat → nat
 
 definition add (x y : nat) : nat := nat_rec x (λn r, succ r) y
 infixl `+`:65 := add
diff --git a/tests/lean/run/nat_bug6.lean b/tests/lean/run/nat_bug6.lean
index 92ce622d92..ee084b35d2 100644
--- a/tests/lean/run/nat_bug6.lean
+++ b/tests/lean/run/nat_bug6.lean
@@ -2,8 +2,8 @@ import standard
 using eq_ops
 
 inductive nat : Type :=
-| zero : nat
-| succ : nat → nat
+zero : nat,
+succ : nat → nat
 
 definition add (x y : nat) : nat := nat_rec x (λn r, succ r) y
 infixl `+`:65 := add
diff --git a/tests/lean/run/nat_bug7.lean b/tests/lean/run/nat_bug7.lean
index d1a58fabe2..4cbd261240 100644
--- a/tests/lean/run/nat_bug7.lean
+++ b/tests/lean/run/nat_bug7.lean
@@ -1,8 +1,8 @@
 import logic
 
 inductive nat : Type :=
-| zero : nat
-| succ : nat → nat
+zero : nat,
+succ : nat → nat
 
 definition add (x y : nat) : nat := nat_rec x (λn r, succ r) y
 infixl `+`:65 := add
@@ -12,4 +12,3 @@ axiom add_right_comm (n m k : nat) : n + m + k = n + k + m
 print "==========================="
 theorem bug (a b c d : nat) : a + b + c + d = a + c + b + d
 := subst (add_right_comm _ _ _) (refl (a + b + c + d))
-
diff --git a/tests/lean/run/opaque_hint_bug.lean b/tests/lean/run/opaque_hint_bug.lean
index 4c9fa08409..d6de03b4b3 100644
--- a/tests/lean/run/opaque_hint_bug.lean
+++ b/tests/lean/run/opaque_hint_bug.lean
@@ -1,8 +1,6 @@
-
-
 inductive list (T : Type) : Type :=
-| nil {} : list T
-| cons : T → list T → list T
+nil {} : list T,
+cons : T → list T → list T
 
 
 section
diff --git a/tests/lean/run/rel.lean b/tests/lean/run/rel.lean
index c4e31e4436..889c70e3d0 100644
--- a/tests/lean/run/rel.lean
+++ b/tests/lean/run/rel.lean
@@ -4,7 +4,7 @@ using relation
 namespace is_equivalence
 
   inductive class {T : Type} (R : T → T → Type) : Prop :=
-  | mk : is_reflexive R → is_symmetric R → is_transitive R → class R
+  mk : is_reflexive R → is_symmetric R → is_transitive R → class R
 
   theorem is_reflexive {T : Type} {R : T → T → Type} {C : class R} : is_reflexive R :=
   class_rec (λx y z, x) C
diff --git a/tests/lean/run/sum_bug.lean b/tests/lean/run/sum_bug.lean
index 1a89cc1c4e..051a1ff5ec 100644
--- a/tests/lean/run/sum_bug.lean
+++ b/tests/lean/run/sum_bug.lean
@@ -10,8 +10,8 @@ namespace sum
 
 -- TODO: take this outside the namespace when the inductive package handles it better
 inductive sum (A B : Type) : Type :=
-| inl : A → sum A B
-| inr : B → sum A B
+inl : A → sum A B,
+inr : B → sum A B
 
 infixr `+`:25 := sum
 
diff --git a/tests/lean/run/tactic23.lean b/tests/lean/run/tactic23.lean
index 7608169ddd..48dda3659d 100644
--- a/tests/lean/run/tactic23.lean
+++ b/tests/lean/run/tactic23.lean
@@ -3,8 +3,8 @@ using num (num pos_num num_rec pos_num_rec)
 using tactic
 
 inductive nat : Type :=
-| zero : nat
-| succ : nat → nat
+zero : nat,
+succ : nat → nat
 
 definition add [inline] (a b : nat) : nat
 := nat_rec a (λ n r, succ r) b
diff --git a/tests/lean/run/tactic26.lean b/tests/lean/run/tactic26.lean
index 4cd72f3a86..164abe54a2 100644
--- a/tests/lean/run/tactic26.lean
+++ b/tests/lean/run/tactic26.lean
@@ -2,8 +2,8 @@ import standard
 using tactic inhabited
 
 inductive sum (A : Type) (B : Type) : Type :=
-| inl  : A → sum A B
-| inr  : B → sum A B
+inl  : A → sum A B,
+inr  : B → sum A B
 
 theorem inl_inhabited {A : Type} (B : Type) (H : inhabited A) : inhabited (sum A B)
 := inhabited_destruct H (λ a, inhabited_mk (inl B a))
diff --git a/tests/lean/run/tactic28.lean b/tests/lean/run/tactic28.lean
index 16a2490a2d..69510bd179 100644
--- a/tests/lean/run/tactic28.lean
+++ b/tests/lean/run/tactic28.lean
@@ -2,8 +2,8 @@ import standard
 using tactic inhabited
 
 inductive sum (A : Type) (B : Type) : Type :=
-| inl  : A → sum A B
-| inr  : B → sum A B
+inl  : A → sum A B,
+inr  : B → sum A B
 
 theorem inl_inhabited {A : Type} (B : Type) (H : inhabited A) : inhabited (sum A B)
 := inhabited_destruct H (λ a, inhabited_mk (inl B a))
diff --git a/tests/lean/run/uni.lean b/tests/lean/run/uni.lean
index 5f6d9af1a9..8935b3638f 100644
--- a/tests/lean/run/uni.lean
+++ b/tests/lean/run/uni.lean
@@ -1,8 +1,8 @@
 import logic
 
 inductive nat : Type :=
-| zero : nat
-| succ : nat → nat
+zero : nat,
+succ : nat → nat
 
 check @nat_rec
 
diff --git a/tests/lean/run/uni2.lean b/tests/lean/run/uni2.lean
index a557e76106..143189e003 100644
--- a/tests/lean/run/uni2.lean
+++ b/tests/lean/run/uni2.lean
@@ -1,8 +1,8 @@
 import logic
 
 inductive nat : Type :=
-| zero : nat
-| succ : nat → nat
+zero : nat,
+succ : nat → nat
 
 variable f : nat → nat
 
diff --git a/tests/lean/run/uni_issue1.lean b/tests/lean/run/uni_issue1.lean
index 2302f4fcf4..5d8198c7c4 100644
--- a/tests/lean/run/uni_issue1.lean
+++ b/tests/lean/run/uni_issue1.lean
@@ -1,8 +1,8 @@
 import standard
 
 inductive nat : Type :=
-| zero : nat
-| succ : nat → nat
+zero : nat,
+succ : nat → nat
 
 definition is_zero (n : nat)
 := nat_rec true (λ n r, false) n
diff --git a/tests/lean/run/univ_bug1.lean b/tests/lean/run/univ_bug1.lean
index 4a947356ab..6f1dcac438 100644
--- a/tests/lean/run/univ_bug1.lean
+++ b/tests/lean/run/univ_bug1.lean
@@ -13,7 +13,7 @@ namespace simp
 
 -- first define a class of homogeneous equality
 inductive simplifies_to {T : Type} (t1 t2 : T) : Prop :=
-| mk : t1 = t2 → simplifies_to t1 t2
+mk : t1 = t2 → simplifies_to t1 t2
 
 theorem get_eq {T : Type} {t1 t2 : T} (C : simplifies_to t1 t2) : t1 = t2 :=
 simplifies_to_rec (λx, x) C
diff --git a/tests/lean/run/univ_bug2.lean b/tests/lean/run/univ_bug2.lean
index a0b8f046ec..cd3885e3d8 100644
--- a/tests/lean/run/univ_bug2.lean
+++ b/tests/lean/run/univ_bug2.lean
@@ -10,7 +10,7 @@ using nat
 namespace simp
 -- first define a class of homogeneous equality
 inductive simplifies_to {T : Type} (t1 t2 : T) : Prop :=
-| mk : t1 = t2 → simplifies_to t1 t2
+mk : t1 = t2 → simplifies_to t1 t2
 
 theorem get_eq {T : Type} {t1 t2 : T} (C : simplifies_to t1 t2) : t1 = t2 :=
 simplifies_to_rec (λx, x) C
diff --git a/tests/lean/run/uuu.lean b/tests/lean/run/uuu.lean
index d05878e5ce..ac8d57c80b 100644
--- a/tests/lean/run/uuu.lean
+++ b/tests/lean/run/uuu.lean
@@ -4,17 +4,17 @@ notation `take`   binders `,` r:(scoped f, f) := r
 
 inductive empty : Type
 inductive unit : Type :=
-| tt : unit
+tt : unit
 inductive nat : Type :=
-| O : nat
-| S : nat → nat
+O : nat,
+S : nat → nat
 
 inductive paths {A : Type} (a : A) : A → Type :=
-| idpath : paths a a
+idpath : paths a a
 
 inductive sum (A : Type) (B : Type) : Type :=
-| inl : A -> sum A B
-| inr : B -> sum A B
+inl : A -> sum A B,
+inr : B -> sum A B
 
 definition coprod := sum
 definition ii1fun {A : Type} (B : Type) (a : A) := inl B a
@@ -23,7 +23,7 @@ definition ii1 {A : Type} {B : Type} (a : A) := inl B a
 definition ii2 {A : Type} {B : Type} (b : B) := inl A b
 
 inductive total2 {T: Type} (P: T → Type) : Type :=
-| tpair : Π (t : T) (tp : P t), total2 P
+tpair : Π (t : T) (tp : P t), total2 P
 
 definition pr1 {T : Type} {P : T → Type} (tp : total2 P) : T
 := total2_rec (λ a b, a) tp
@@ -31,7 +31,7 @@ definition pr2 {T : Type} {P : T → Type} (tp : total2 P) : P (pr1 tp)
 := total2_rec (λ a b, b) tp
 
 inductive Phant (T : Type) : Type :=
-| phant : Phant T
+phant : Phant T
 
 definition fromempty {X : Type} : empty → X
 := λe, empty_rec (λe, X) e
diff --git a/tests/lean/slow/list_elab2.lean b/tests/lean/slow/list_elab2.lean
index 1550449a2a..0c0f882c3c 100644
--- a/tests/lean/slow/list_elab2.lean
+++ b/tests/lean/slow/list_elab2.lean
@@ -22,8 +22,8 @@ namespace list
 -- ----
 
 inductive list (T : Type) : Type :=
-| nil {} : list T
-| cons : T → list T → list T
+nil {} : list T,
+cons : T → list T → list T
 
 infix `::` : 65 := cons
 
diff --git a/tests/lean/slow/nat_wo_hints.lean b/tests/lean/slow/nat_wo_hints.lean
index 74781a12d9..523f18dacc 100644
--- a/tests/lean/slow/nat_wo_hints.lean
+++ b/tests/lean/slow/nat_wo_hints.lean
@@ -9,8 +9,8 @@ using decidable
 
 namespace nat
 inductive nat : Type :=
-| zero : nat
-| succ : nat → nat
+zero : nat,
+succ : nat → nat
 
 notation `ℕ`:max := nat
 
diff --git a/tests/lean/slow/path_groupoids.lean b/tests/lean/slow/path_groupoids.lean
index feeab6dda5..8eaedfcc7b 100644
--- a/tests/lean/slow/path_groupoids.lean
+++ b/tests/lean/slow/path_groupoids.lean
@@ -14,7 +14,7 @@ infixl `∘`:60 := compose
 -- ----
 
 inductive path {A : Type} (a : A) : A → Type :=
-| idpath : path a a
+idpath : path a a
 
 infix `≈`:50 := path
 -- TODO: is this right?