diff --git a/library/data/bool.lean b/library/data/bool.lean
index 40f07b5f8f..08aa6a9a5e 100644
--- a/library/data/bool.lean
+++ b/library/data/bool.lean
@@ -13,13 +13,13 @@ tt : bool
 namespace bool
 
 theorem cases_on {p : bool → Prop} (b : bool) (H0 : p ff) (H1 : p tt) : p b :=
-bool_rec H0 H1 b
+rec H0 H1 b
 
 theorem bool_inhabited [instance] : inhabited bool :=
 inhabited_mk ff
 
 definition cond {A : Type} (b : bool) (t e : A) :=
-bool_rec e t b
+rec e t b
 
 theorem dichotomy (b : bool) : b = ff ∨ b = tt :=
 cases_on b (or_inl (refl ff)) (or_inr (refl tt))
@@ -38,13 +38,13 @@ assume H : ff = tt, absurd
   true_ne_false
 
 theorem decidable_eq [instance] (a b : bool) : decidable (a = b) :=
-bool_rec
-  (bool_rec (inl (refl ff)) (inr ff_ne_tt) b)
-  (bool_rec (inr (ne_symm ff_ne_tt)) (inl (refl tt)) b)
+rec
+  (rec (inl (refl ff)) (inr ff_ne_tt) b)
+  (rec (inr (ne_symm ff_ne_tt)) (inl (refl tt)) b)
   a
 
 definition bor (a b : bool) :=
-bool_rec (bool_rec ff tt b) tt a
+rec (rec ff tt b) tt a
 
 theorem bor_tt_left (a : bool) : bor tt a = tt :=
 rfl
@@ -77,7 +77,7 @@ cases_on a
                  ...   = tt || (b || c) : bor_tt_left (b || c)⁻¹)
 
 theorem bor_to_or {a b : bool} : a || b = tt → a = tt ∨ b = tt :=
-bool_rec
+rec
   (assume H : ff || b = tt,
     have Hb : b = tt, from (bor_ff_left b) ▸ H,
     or_inr Hb)
@@ -85,7 +85,7 @@ bool_rec
   a
 
 definition band (a b : bool) :=
-bool_rec ff (bool_rec ff tt b) a
+rec ff (rec ff tt b) a
 
 infixl `&&` := band
 
@@ -130,7 +130,7 @@ or_elim (dichotomy a)
 theorem band_eq_tt_elim_right {a b : bool} (H : a && b = tt) : b = tt :=
 band_eq_tt_elim_left (trans (band_comm b a) H)
 
-definition bnot (a : bool) := bool_rec tt ff a
+definition bnot (a : bool) := rec tt ff a
 
 notation `!` x:max := bnot x
 
diff --git a/library/data/empty.lean b/library/data/empty.lean
index c686a6dd37..74a3a5d5b5 100644
--- a/library/data/empty.lean
+++ b/library/data/empty.lean
@@ -9,4 +9,4 @@
 
 inductive empty : Type
 
-theorem empty_elim (A : Type) (H : empty) : A := empty_rec (λe, A) H
+theorem empty_elim (A : Type) (H : empty) : A := empty.rec (λe, A) H
diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean
index 8b00063999..d609970324 100644
--- a/library/data/list/basic.lean
+++ b/library/data/list/basic.lean
@@ -18,15 +18,14 @@ open nat
 open eq_ops
 open helper_tactics
 
-namespace list
-
--- Type
--- ----
-
 inductive list (T : Type) : Type :=
 nil {} : list T,
 cons   : T → list T → list T
 
+namespace list
+
+-- Type
+-- ----
 infix `::` := cons
 
 section
@@ -35,7 +34,7 @@ variable {T : Type}
 
 theorem induction_on [protected] {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 :=
-list_rec Hnil Hind l
+rec Hnil Hind l
 
 theorem cases_on [protected] {P : list T → Prop} (l : list T) (Hnil : P nil)
     (Hcons : forall x : T, forall l : list T, P (cons x l)) : P l :=
@@ -48,7 +47,7 @@ notation `[` l:(foldr `,` (h t, cons h t) nil) `]` := l
 -- ------
 
 definition concat (s t : list T) : list T :=
-list_rec t (fun x : T, fun l : list T, fun u : list T, cons x u) s
+rec t (fun x : T, fun l : list T, fun u : list T, cons x u) s
 
 infixl `++` : 65 := concat
 
@@ -73,7 +72,7 @@ induction_on s rfl
 -- Length
 -- ------
 
-definition length : list T → ℕ := list_rec 0 (fun x l m, succ m)
+definition length : list T → ℕ := rec 0 (fun x l m, succ m)
 
 theorem length_nil : length (@nil T) = 0 := rfl
 
@@ -98,7 +97,7 @@ induction_on s
 -- Append
 -- ------
 
-definition append (x : T) : list T → list T := list_rec [x] (fun y l l', y :: l')
+definition append (x : T) : list T → list T := rec [x] (fun y l l', y :: l')
 
 theorem append_nil {x : T} : append x nil = [x]
 
@@ -111,7 +110,7 @@ theorem append_eq_concat  {x : T} {l : list T} : append x l = l ++ [x]
 -- Reverse
 -- -------
 
-definition reverse : list T → list T := list_rec nil (fun x l r, r ++ [x])
+definition reverse : list T → list T := rec nil (fun x l r, r ++ [x])
 
 theorem reverse_nil : reverse (@nil T) = nil
 
@@ -153,7 +152,7 @@ induction_on l rfl
 -- Head and tail
 -- -------------
 
-definition head (x : T) : list T → T := list_rec x (fun x l h, x)
+definition head (x : T) : list T → T := rec x (fun x l h, x)
 
 theorem head_nil {x : T} : head x (@nil T) = x
 
@@ -168,7 +167,7 @@ cases_on s
         ... = x                                                   : {head_cons}
         ... = head x (cons x s)                                   : {head_cons⁻¹})
 
-definition tail : list T → list T := list_rec nil (fun x l b, l)
+definition tail : list T → list T := rec nil (fun x l b, l)
 
 theorem tail_nil : tail (@nil T) = nil
 
@@ -182,7 +181,7 @@ cases_on l
 -- List membership
 -- ---------------
 
-definition mem (x : T) : list T → Prop := list_rec false (fun y l H, x = y ∨ H)
+definition mem (x : T) : list T → Prop := rec false (fun y l H, x = y ∨ H)
 
 infix `∈` := mem
 
@@ -238,7 +237,7 @@ induction_on l
 
 -- to do this: need decidability of = for nat
 -- definition find (x : T) : list T → nat
--- := list_rec 0 (fun y l b, if x = y then 0 else succ b)
+-- := rec 0 (fun y l b, if x = y then 0 else succ b)
 
 -- theorem find_nil (f : T) : find f nil = 0
 -- :=refl _
@@ -272,7 +271,7 @@ induction_on l
 -- -----------
 
 definition nth (x : T) (l : list T) (n : ℕ) : T :=
-nat_rec (λl, head x l) (λm f l, f (tail l)) n l
+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
 
diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean
index e889e19788..5214f93933 100644
--- a/library/data/nat/basic.lean
+++ b/library/data/nat/basic.lean
@@ -16,36 +16,36 @@ open helper_tactics
 
 -- Definition of the type
 -- ----------------------
-
-namespace nat
 inductive nat : Type :=
   zero : nat,
   succ : nat → nat
 
+namespace nat
+
 notation `ℕ` := nat
 
-theorem rec_zero {P : ℕ → Type} (x : P zero) (f : ∀m, P m → P (succ m)) : nat_rec x f zero = x
+theorem rec_zero {P : ℕ → Type} (x : P zero) (f : ∀m, P m → P (succ m)) : nat.rec x f zero = x
 
 theorem rec_succ {P : ℕ → Type} (x : P zero) (f : ∀m, P m → P (succ m)) (n : ℕ) :
-  nat_rec x f (succ n) = f n (nat_rec x f n)
+  nat.rec x f (succ n) = f n (nat.rec x f n)
 
 theorem induction_on [protected] {P : ℕ → Prop} (a : ℕ) (H1 : P zero) (H2 : ∀ (n : ℕ) (IH : P n), P (succ n)) :
   P a :=
-nat_rec H1 H2 a
+nat.rec H1 H2 a
 
 definition rec_on [protected] {P : ℕ → Type} (n : ℕ) (H1 : P zero) (H2 : ∀m, P m → P (succ m)) : P n :=
-nat_rec H1 H2 n
+nat.rec H1 H2 n
 
 
 -- Coercion from num
 -- -----------------
 
 abbreviation plus (x y : ℕ) : ℕ :=
-nat_rec x (λ n r, succ r) y
+nat.rec x (λ n r, succ r) y
 
 definition to_nat [coercion] [inline] (n : num) : ℕ :=
-num_rec zero
-    (λ n, pos_num_rec (succ zero) (λ n r, plus r (plus r (succ zero))) (λ n r, plus r r) n) n
+num.num.rec zero
+    (λ n, num.pos_num.rec (succ zero) (λ n r, plus r (plus r (succ zero))) (λ n r, plus r r) n) n
 
 
 -- Successor and predecessor
@@ -54,7 +54,7 @@ num_rec zero
 theorem succ_ne_zero {n : ℕ} : succ n ≠ 0 :=
 assume H : succ n = 0,
 have H2 : true = false, from
-  let f := (nat_rec false (fun a b, true)) in
+  let f := (nat.rec false (fun a b, true)) in
     calc
       true = f (succ n) : rfl
        ... = f 0        : {H}
@@ -63,7 +63,7 @@ absurd H2 true_ne_false
 
 -- add_rewrite succ_ne_zero
 
-definition pred (n : ℕ) := nat_rec 0 (fun m x, m) n
+definition pred (n : ℕ) := nat.rec 0 (fun m x, m) n
 
 theorem pred_zero : pred 0 = 0
 
@@ -255,12 +255,12 @@ add_zero_left ▸ add_succ_left
 -- TODO: rename? remove?
 theorem induction_plus_one {P : nat → Prop} (a : ℕ) (H1 : P 0)
     (H2 : ∀ (n : ℕ) (IH : P n), P (n + 1)) : P a :=
-nat_rec H1 (take n IH, add_one ▸ (H2 n IH)) a
+nat.rec H1 (take n IH, add_one ▸ (H2 n IH)) a
 
 -- Multiplication
 -- --------------
 
-definition mul (n m : ℕ) := nat_rec 0 (fun m x, x + n) m
+definition mul (n m : ℕ) := nat.rec 0 (fun m x, x + n) m
 infixl `*` := mul
 
 theorem mul_zero_right {n : ℕ} : n * 0 = 0
diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean
index 9714d0e701..d88e1ac40a 100644
--- a/library/data/nat/div.lean
+++ b/library/data/nat/div.lean
@@ -54,7 +54,7 @@ if_neg H
 
 definition rec_measure_aux {dom codom : Type} (default : codom) (measure : dom → ℕ)
     (rec_val : dom → (dom → codom) → codom) : ℕ → dom → codom :=
-nat_rec (λx, default) (λm g x, if measure x < succ m then rec_val x g else default)
+rec (λx, default) (λm g x, if measure x < succ m then rec_val x g else default)
 
 definition rec_measure {dom codom : Type} (default : codom) (measure : dom → ℕ)
     (rec_val : dom → (dom → codom) → codom) (x : dom) : codom :=
diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean
index 7b586ccc4c..f1c28b62e3 100644
--- a/library/data/nat/order.lean
+++ b/library/data/nat/order.lean
@@ -12,7 +12,6 @@ import tools.fake_simplifier
 
 open nat eq_ops tactic
 open fake_simplifier
-open decidable (decidable inl inr)
 
 namespace nat
 
diff --git a/library/data/nat/sub.lean b/library/data/nat/sub.lean
index 1764eb156f..560e68f1e6 100644
--- a/library/data/nat/sub.lean
+++ b/library/data/nat/sub.lean
@@ -19,7 +19,7 @@ namespace nat
 -- subtraction
 -- -----------
 
-definition sub (n m : ℕ) : nat := nat_rec n (fun m x, pred x) m
+definition sub (n m : ℕ) : nat := rec n (fun m x, pred x) m
 infixl `-` := sub
 
 theorem sub_zero_right {n : ℕ} : n - 0 = n
diff --git a/library/data/num.lean b/library/data/num.lean
index fb91d77fa9..c7255d9396 100644
--- a/library/data/num.lean
+++ b/library/data/num.lean
@@ -7,7 +7,6 @@
 import logic.classes.inhabited
 
 namespace num
-
 -- pos_num and num are two auxiliary datatypes used when parsing numerals such as 13, 0, 26.
 -- 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).
diff --git a/library/data/option.lean b/library/data/option.lean
index 7286ace555..06922e8b4c 100644
--- a/library/data/option.lean
+++ b/library/data/option.lean
@@ -13,14 +13,14 @@ some    : A → option A
 
 theorem induction_on [protected] {A : Type} {p : option A → Prop} (o : option A)
   (H1 : p none) (H2 : ∀a, p (some a)) : p o :=
-option_rec H1 H2 o
+option.rec H1 H2 o
 
 definition rec_on [protected] {A : Type} {C : option A → Type} (o : option A)
   (H1 : C none) (H2 : ∀a, C (some a)) : C o :=
-option_rec H1 H2 o
+option.rec H1 H2 o
 
 definition is_none {A : Type} (o : option A) : Prop :=
-option_rec true (λ a, false) o
+option.rec true (λ a, false) o
 
 theorem is_none_none {A : Type} : is_none (@none A) :=
 trivial
@@ -34,7 +34,7 @@ assume H : none = some a, absurd
   (not_is_none_some a)
 
 theorem some_inj {A : Type} {a₁ a₂ : A} (H : some a₁ = some a₂) : a₁ = a₂ :=
-congr_arg (option_rec a₁ (λ a, a)) H
+congr_arg (option.rec a₁ (λ a, a)) H
 
 theorem option_inhabited [instance] (A : Type) : inhabited (option A) :=
 inhabited_mk none
diff --git a/library/data/prod.lean b/library/data/prod.lean
index 02b350586e..4d8ff8b612 100644
--- a/library/data/prod.lean
+++ b/library/data/prod.lean
@@ -25,8 +25,8 @@ section
 
   parameters {A B : Type}
 
-  abbreviation pr1 (p : prod A B) := prod_rec (λ x y, x) p
-  abbreviation pr2 (p : prod A B) := prod_rec (λ x y, y) p
+  abbreviation pr1 (p : prod A B) := rec (λ x y, x) p
+  abbreviation pr2 (p : prod A B) := rec (λ x y, y) p
 
   theorem pr1_pair (a : A) (b : B) : pr1 (a, b) = a :=
   rfl
@@ -34,18 +34,17 @@ section
   theorem pr2_pair (a : A) (b : B) : pr2 (a, b) = b :=
   rfl
 
-  -- TODO: remove prefix when we can protect it
-  theorem pair_destruct {P : A × B → Prop} (p : A × B) (H : ∀a b, P (a, b)) : P p :=
-  prod_rec H p
+  theorem destruct [protected] {P : A × B → Prop} (p : A × B) (H : ∀a b, P (a, b)) : P p :=
+  rec H p
 
   theorem prod_ext (p : prod A B) : pair (pr1 p) (pr2 p) = p :=
-  pair_destruct p (λx y, refl (x, y))
+  destruct p (λx y, refl (x, y))
 
   theorem pair_eq {a1 a2 : A} {b1 b2 : B} (H1 : a1 = a2) (H2 : b1 = b2) : (a1, b1) = (a2, b2) :=
   subst H1 (subst H2 rfl)
 
   theorem prod_eq {p1 p2 : prod A B} : ∀ (H1 : pr1 p1 = pr1 p2) (H2 : pr2 p1 = pr2 p2), p1 = p2 :=
-  pair_destruct p1 (take a1 b1, pair_destruct p2 (take a2 b2 H1 H2, pair_eq H1 H2))
+  destruct p1 (take a1 b1, destruct p2 (take a2 b2 H1 H2, pair_eq H1 H2))
 
   theorem prod_inhabited [instance] (H1 : inhabited A) (H2 : inhabited B) : inhabited (prod A B) :=
   inhabited_destruct H1 (λa, inhabited_destruct H2 (λb, inhabited_mk (pair a b)))
diff --git a/library/data/quotient/aux.lean b/library/data/quotient/aux.lean
index 896ad88eee..e0fe7a31e2 100644
--- a/library/data/quotient/aux.lean
+++ b/library/data/quotient/aux.lean
@@ -26,7 +26,7 @@ theorem flip_pr1 {A B : Type} (a : A × B) : pr1 (flip a) = pr2 a := rfl
 theorem flip_pr2 {A B : Type} (a : A × B) : pr2 (flip a) = pr1 a := rfl
 
 theorem flip_flip {A B : Type} (a : A × B) : flip (flip a) = a :=
-pair_destruct a (take x y, rfl)
+prod.destruct a (take x y, rfl)
 
 theorem P_flip {A B : Type} {P : A → B → Prop} {a : A × B} (H : P (pr1 a) (pr2 a))
   : P (pr2 (flip a)) (pr1 (flip a)) :=
diff --git a/library/data/quotient/basic.lean b/library/data/quotient/basic.lean
index f61a4d5f8e..93169a2685 100644
--- a/library/data/quotient/basic.lean
+++ b/library/data/quotient/basic.lean
@@ -222,7 +222,7 @@ theorem image_elt_of {A B : Type} {f : A → B} (u : image f) : ∃a, f a = elt_
 has_property u
 
 theorem fun_image_surj {A B : Type} {f : A → B} (u : image f) : ∃a, fun_image f a = u :=
-subtype_destruct u
+subtype.destruct u
   (take (b : B) (H : ∃a, f a = b),
     obtain a (H': f a = b), from H,
     (exists_intro a (tag_eq H')))
diff --git a/library/data/sigma.lean b/library/data/sigma.lean
index 8c15151aca..841290a50c 100644
--- a/library/data/sigma.lean
+++ b/library/data/sigma.lean
@@ -17,15 +17,15 @@ section
 
   parameters {A : Type} {B : A → Type}
 
-  abbreviation dpr1 (p : Σ x, B x) : A := sigma_rec (λ a b, a) p
-  abbreviation dpr2 {A : Type} {B : A → Type} (p : Σ x, B x) : B (dpr1 p) := sigma_rec (λ a b, b) p
+  abbreviation dpr1 (p : Σ x, B x) : A := rec (λ a b, a) p
+  abbreviation dpr2 {A : Type} {B : A → Type} (p : Σ x, B x) : B (dpr1 p) := rec (λ a b, b) p
 
   theorem dpr1_dpair (a : A) (b : B a) : dpr1 (dpair a b) = a := refl a
   theorem dpr2_dpair (a : A) (b : B a) : dpr2 (dpair a b) = b := refl b
 
   -- TODO: remove prefix when we can protect it
   theorem sigma_destruct {P : sigma B → Prop} (p : sigma B) (H : ∀a b, P (dpair a b)) : P p :=
-  sigma_rec H p
+  rec H p
 
   theorem dpair_ext (p : sigma B) : dpair (dpr1 p) (dpr2 p) = p :=
   sigma_destruct p (take a b, rfl)
@@ -34,7 +34,7 @@ section
   theorem dpair_eq {a1 a2 : A} {b1 : B a1} {b2 : B a2} (H1 : a1 = a2) (H2 : eq_rec_on H1 b1 = b2) :
     dpair a1 b1 = dpair a2 b2 :=
   (show ∀(b2 : B a2) (H1 : a1 = a2) (H2 : eq_rec_on H1 b1 = b2), dpair a1 b1 = dpair a2 b2, from
-    eq_rec
+    eq.rec
       (take (b2' : B a1),
         assume (H1' : a1 = a1),
         assume (H2' : eq_rec_on H1' b1 = b2'),
diff --git a/library/data/subtype.lean b/library/data/subtype.lean
index cd8af4407c..636b350ea9 100644
--- a/library/data/subtype.lean
+++ b/library/data/subtype.lean
@@ -18,31 +18,31 @@ section
   parameter {P : A → Prop}
 
   -- TODO: make this a coercion?
-  definition  elt_of (a : {x, P x}) : A := subtype_rec (λ x y, x) a
-  theorem has_property (a : {x, P x}) : P (elt_of a) := subtype_rec (λ x y, y) a
+  definition  elt_of (a : {x, P x}) : A := rec (λ x y, x) a
+  theorem has_property (a : {x, P x}) : P (elt_of a) := rec (λ x y, y) a
 
   theorem elt_of_tag (a : A) (H : P a) : elt_of (tag a H) = a := refl a
 
-  theorem subtype_destruct {Q : {x, P x} → Prop} (a : {x, P x})
+  theorem destruct [protected] {Q : {x, P x} → Prop} (a : {x, P x})
       (H : ∀(x : A) (H1 : P x), Q (tag x H1)) : Q a :=
-    subtype_rec H a
+    rec H a
 
   theorem tag_irrelevant {a : A} (H1 H2 : P a) : tag a H1 = tag a H2 :=
   rfl
 
   theorem tag_elt_of (a : subtype P) : ∀(H : P (elt_of a)), tag (elt_of a) H = a :=
-    subtype_destruct a (take (x : A) (H1 : P x) (H2 : P x), rfl)
+    destruct a (take (x : A) (H1 : P x) (H2 : P x), rfl)
 
   theorem tag_eq {a1 a2 : A} {H1 : P a1} {H2 : P a2} (H3 : a1 = a2) : tag a1 H1 = tag a2 H2 :=
   subst H3 (take H2, tag_irrelevant H1 H2) H2
 
   theorem subtype_eq {a1 a2 : {x, P x}} : ∀(H : elt_of a1 = elt_of a2), a1 = a2 :=
-  subtype_destruct a1 (take x1 H1, subtype_destruct a2 (take x2 H2 H, tag_eq H))
+  destruct a1 (take x1 H1, destruct a2 (take x2 H2 H, tag_eq H))
 
-  theorem subtype_inhabited {a : A} (H : P a) : inhabited {x, P x} :=
+  theorem subtype_inhabited [instance] {a : A} (H : P a) : inhabited {x, P x} :=
   inhabited_mk (tag a H)
 
-  theorem subtype_eq_decidable (a1 a2 : {x, P x})
+  theorem eq_decidable [protected] [instance] (a1 a2 : {x, P x})
     (H : decidable (elt_of a1 = elt_of a2)) : decidable (a1 = a2) :=
   have H1 : (a1 = a2) ↔ (elt_of a1 = elt_of a2), from
     iff_intro (assume H, subst H rfl) (assume H, subtype_eq H),
@@ -50,7 +50,4 @@ section
 
 end
 
-instance subtype_inhabited
-instance subtype_eq_decidable
-
 end subtype
diff --git a/library/data/sum.lean b/library/data/sum.lean
index 931c6e2d0a..7e50e12ec9 100644
--- a/library/data/sum.lean
+++ b/library/data/sum.lean
@@ -26,11 +26,11 @@ end sum_plus_notation
 
 abbreviation rec_on [protected] {A B : Type} {C : (A ⊎ B) → Type} (s : A ⊎ B)
   (H1 : ∀a : A, C (inl B a)) (H2 : ∀b : B, C (inr A b)) : C s :=
-sum_rec H1 H2 s
+rec H1 H2 s
 
 abbreviation cases_on [protected] {A B : Type} {P : (A ⊎ B) → Prop} (s : A ⊎ B)
   (H1 : ∀a : A, P (inl B a)) (H2 : ∀b : B, P (inr A b)) : P s :=
-sum_rec H1 H2 s
+rec H1 H2 s
 
 -- Here is the trick for the theorems that follow:
 -- Fixing a1, "f s" is a recursive description of "inl B a1 = s".
diff --git a/library/data/unit.lean b/library/data/unit.lean
index 19dfca8d8f..53a13e0d5a 100644
--- a/library/data/unit.lean
+++ b/library/data/unit.lean
@@ -14,7 +14,7 @@ star : unit
 notation `⋆`:max := star
 
 theorem unit_eq (a b : unit) : a = b :=
-unit_rec (unit_rec (refl ⋆) b) a
+rec (rec rfl b) a
 
 theorem unit_eq_star (a : unit) : a = star :=
 unit_eq a star
diff --git a/library/hott/equiv.lean b/library/hott/equiv.lean
index e2caebce8d..470e718ba6 100644
--- a/library/hott/equiv.lean
+++ b/library/hott/equiv.lean
@@ -24,18 +24,18 @@ IsEquiv_mk : Π
 IsEquiv f
 
 definition equiv_inv {A B : Type} {f : A → B} (H : IsEquiv f) : B → A :=
-IsEquiv_rec (λequiv_inv eisretr eissect eisadj, equiv_inv) H
+IsEquiv.rec (λequiv_inv eisretr eissect eisadj, equiv_inv) H
 
 -- TODO: note: does not type check without giving the type
 definition eisretr {A B : Type} {f : A → B} (H : IsEquiv f) : Sect (equiv_inv H) f :=
-IsEquiv_rec (λequiv_inv eisretr eissect eisadj, eisretr) H
+IsEquiv.rec (λequiv_inv eisretr eissect eisadj, eisretr) H
 
 definition eissect {A B : Type} {f : A → B} (H : IsEquiv f) : Sect f (equiv_inv H) :=
-IsEquiv_rec (λequiv_inv eisretr eissect eisadj, eissect) H
+IsEquiv.rec (λequiv_inv eisretr eissect eisadj, eissect) H
 
 definition eisadj {A B : Type} {f : A → B} (H : IsEquiv f) :
   Πx, eisretr H (f x) ≈ ap f (eissect H x) :=
-IsEquiv_rec (λequiv_inv eisretr eissect eisadj, eisadj) H
+IsEquiv.rec (λequiv_inv eisretr eissect eisadj, eisadj) H
 
 -- Structure Equiv
 
@@ -46,13 +46,13 @@ Equiv_mk : Π
 Equiv A B
 
 definition equiv_fun {A B : Type} (e : Equiv A B) : A → B :=
-Equiv_rec (λequiv_fun equiv_isequiv, equiv_fun) e
+Equiv.rec (λequiv_fun equiv_isequiv, equiv_fun) e
 
 -- TODO: use a type class instead?
 coercion equiv_fun : Equiv
 
 definition equiv_isequiv [coercion] {A B : Type} (e : Equiv A B) : IsEquiv (equiv_fun e) :=
-Equiv_rec (λequiv_fun equiv_isequiv, equiv_isequiv) e
+Equiv.rec (λequiv_fun equiv_isequiv, equiv_isequiv) e
 
 -- coercion equiv_isequiv
 
diff --git a/library/hott/path.lean b/library/hott/path.lean
index ab7d2fa78f..96d7bc8260 100644
--- a/library/hott/path.lean
+++ b/library/hott/path.lean
@@ -25,7 +25,7 @@ notation `idp`:max := idpath _    -- TODO: can we / should we use `1`?
 namespace path
   abbreviation induction_on [protected] {A : Type} {a b : A} (p : a ≈ b)
     {C : Π (b : A) (p : a ≈ b), Type} (H : C a (idpath a)) : C b p :=
-  path_rec H p
+  path.rec H p
 end path
 
 
@@ -36,11 +36,11 @@ open path (induction_on)
 -- -------------------------
 
 definition concat {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : x ≈ z :=
-path_rec (λu, u) q p
+path.rec (λu, u) q p
 
 -- TODO: should this be an abbreviation?
 definition inverse {A : Type} {x y : A} (p : x ≈ y) : y ≈ x :=
-path_rec (idpath x) p
+path.rec (idpath x) p
 
 infixl `@`:75 := concat
 postfix `^`:100 := inverse
diff --git a/library/hott/trunc.lean b/library/hott/trunc.lean
index f8637a8fbe..b5ccad61aa 100644
--- a/library/hott/trunc.lean
+++ b/library/hott/trunc.lean
@@ -15,10 +15,10 @@ Contr_mk : Π
   (contr : Πy : A, center ≈ y),
 Contr A
 
-definition center {A : Type} (C : Contr A) : A := Contr_rec (λcenter contr, center) C
+definition center {A : Type} (C : Contr A) : A := Contr.rec (λcenter contr, center) C
 
 definition contr {A : Type} (C : Contr A) : Πy : A, center C ≈ y :=
-Contr_rec (λcenter contr, contr) C
+Contr.rec (λcenter contr, contr) C
 
 inductive trunc_index : Type :=
 minus_two : trunc_index,
@@ -28,11 +28,11 @@ trunc_S : trunc_index → trunc_index
 
 -- TODO: note in the Coq version, there is an internal version
 definition IsTrunc (n : trunc_index) : Type → Type :=
-trunc_index_rec (λA, Contr A) (λn trunc_n A, (Π(x y : A), trunc_n (x ≈ y))) n
+trunc_index.rec (λA, Contr A) (λn trunc_n A, (Π(x y : A), trunc_n (x ≈ y))) n
 
 -- TODO: in the Coq version, this is notation
 abbreviation minus_one := trunc_S minus_two
 abbreviation IsHProp := IsTrunc minus_one
 abbreviation IsHSet := IsTrunc (trunc_S minus_one)
 
-prefix `!`:75 := center
\ No newline at end of file
+prefix `!`:75 := center
diff --git a/library/logic/classes/decidable.lean b/library/logic/classes/decidable.lean
index 06d3fbb9b1..42494e5426 100644
--- a/library/logic/classes/decidable.lean
+++ b/library/logic/classes/decidable.lean
@@ -4,12 +4,12 @@
 
 import logic.core.connectives
 
-namespace decidable
-
 inductive decidable (p : Prop) : Type :=
 inl : p  → decidable p,
 inr : ¬p → decidable p
 
+namespace decidable
+
 theorem true_decidable [instance] : decidable true :=
 inl trivial
 
@@ -17,19 +17,19 @@ theorem false_decidable [instance] : decidable false :=
 inr not_false_trivial
 
 theorem induction_on [protected] {p : Prop} {C : Prop} (H : decidable p) (H1 : p → C) (H2 : ¬p → C) : C :=
-decidable_rec H1 H2 H
+decidable.rec H1 H2 H
 
 definition rec_on [protected] [inline] {p : Prop} {C : Type} (H : decidable p) (H1 : p → C) (H2 : ¬p → C) :
   C :=
-decidable_rec H1 H2 H
+decidable.rec H1 H2 H
 
 theorem irrelevant {p : Prop} (d1 d2 : decidable p) : d1 = d2 :=
-decidable_rec
-  (assume Hp1 : p, decidable_rec
+decidable.rec
+  (assume Hp1 : p, decidable.rec
     (assume Hp2  : p,  congr_arg inl (refl Hp1)) -- using proof irrelevance for Prop
     (assume Hnp2 : ¬p, absurd Hp1 Hnp2)
     d2)
-  (assume Hnp1 : ¬p, decidable_rec
+  (assume Hnp1 : ¬p, decidable.rec
     (assume Hp2  : p,  absurd Hp2 Hnp1)
     (assume Hnp2 : ¬p, congr_arg inr (refl Hnp1)) -- using proof irrelevance for Prop
     d2)
diff --git a/library/logic/classes/inhabited.lean b/library/logic/classes/inhabited.lean
index ebd994e98b..3467a35d0f 100644
--- a/library/logic/classes/inhabited.lean
+++ b/library/logic/classes/inhabited.lean
@@ -10,7 +10,7 @@ inhabited_mk : A → inhabited A
 namespace inhabited
 
 definition inhabited_destruct {A : Type} {B : Type} (H1 : inhabited A) (H2 : A → B) : B :=
-inhabited_rec H2 H1
+inhabited.rec H2 H1
 
 definition Prop_inhabited [instance] : inhabited Prop :=
 inhabited_mk true
diff --git a/library/logic/classes/nonempty.lean b/library/logic/classes/nonempty.lean
index 5ed93edcac..e7b2c7ae60 100644
--- a/library/logic/classes/nonempty.lean
+++ b/library/logic/classes/nonempty.lean
@@ -12,7 +12,7 @@ inductive nonempty (A : Type) : Prop :=
 nonempty_intro : A → nonempty A
 
 definition nonempty_elim {A : Type} {B : Prop} (H1 : nonempty A) (H2 : A → B) : B :=
-nonempty_rec H2 H1
+nonempty.rec H2 H1
 
 theorem inhabited_imp_nonempty [instance] {A : Type} (H : inhabited A) : nonempty A :=
 nonempty_intro (default A)
diff --git a/library/logic/core/cast.lean b/library/logic/core/cast.lean
index afe8d8ad06..39abcadb6d 100644
--- a/library/logic/core/cast.lean
+++ b/library/logic/core/cast.lean
@@ -9,7 +9,7 @@ import .eq .quantifiers
 open eq_ops
 
 definition cast {A B : Type} (H : A = B) (a : A) : B :=
-eq_rec a H
+eq.rec a H
 
 theorem cast_refl {A : Type} (a : A) : cast (refl A) a = a :=
 refl (cast (refl A) a)
diff --git a/library/logic/core/connectives.lean b/library/logic/core/connectives.lean
index 7b669fbd1e..aa79f4d1c3 100644
--- a/library/logic/core/connectives.lean
+++ b/library/logic/core/connectives.lean
@@ -14,13 +14,13 @@ infixr `/\` := and
 infixr `∧` := and
 
 theorem and_elim {a b c : Prop} (H1 : a ∧ b) (H2 : a → b → c) : c :=
-and_rec H2 H1
+and.rec H2 H1
 
 theorem and_elim_left {a b : Prop} (H : a ∧ b) : a  :=
-and_rec (λa b, a) H
+and.rec (λa b, a) H
 
 theorem and_elim_right {a b : Prop} (H : a ∧ b) : b :=
-and_rec (λa b, b) H
+and.rec (λa b, b) H
 
 theorem and_swap {a b : Prop} (H : a ∧ b) : b ∧ a :=
 and_intro (and_elim_right H) (and_elim_left H)
@@ -55,7 +55,7 @@ theorem or_inl {a b : Prop} (Ha : a) : a ∨ b := or_intro_left b Ha
 theorem or_inr {a b : Prop} (Hb : b) : a ∨ b := or_intro_right a Hb
 
 theorem or_elim {a b c : Prop} (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c :=
-or_rec H2 H3 H1
+or.rec H2 H3 H1
 
 theorem resolve_right {a b : Prop} (H1 : a ∨ b) (H2 : ¬a) : b :=
 or_elim H1 (assume Ha, absurd Ha H2) (assume Hb, Hb)
@@ -103,7 +103,7 @@ theorem iff_def {a b : Prop} : (a ↔ b) = ((a → b) ∧ (b → a)) := rfl
 
 theorem iff_intro {a b : Prop} (H1 : a → b) (H2 : b → a) : a ↔ b := and_intro H1 H2
 
-theorem iff_elim {a b c : Prop} (H1 : (a → b) → (b → a) → c) (H2 : a ↔ b) : c := and_rec H1 H2
+theorem iff_elim {a b c : Prop} (H1 : (a → b) → (b → a) → c) (H2 : a ↔ b) : c := and.rec H1 H2
 
 theorem iff_elim_left {a b : Prop} (H : a ↔ b) : a → b :=
 iff_elim (assume H1 H2, H1) H
diff --git a/library/logic/core/eq.lean b/library/logic/core/eq.lean
index d4c32dfeac..2bfccdc8b1 100644
--- a/library/logic/core/eq.lean
+++ b/library/logic/core/eq.lean
@@ -23,7 +23,7 @@ theorem eq_id_refl {A : Type} {a : A} (H1 : a = a) : H1 = (refl a) := rfl
 theorem eq_irrel {A : Type} {a b : A} (H1 H2 : a = b) : H1 = H2 := rfl
 
 theorem subst {A : Type} {a b : A} {P : A → Prop} (H1 : a = b) (H2 : P a) : P b :=
-eq_rec H2 H1
+eq.rec H2 H1
 
 theorem trans {A : Type} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c :=
 subst H2 H1
@@ -48,12 +48,12 @@ assume H : true = false,
 
 -- eq_rec with arguments swapped, for transporting an element of a dependent type
 definition eq_rec_on {A : Type} {a1 a2 : A} {B : A → Type} (H1 : a1 = a2) (H2 : B a1) : B a2 :=
-eq_rec H2 H1
+eq.rec H2 H1
 
 theorem eq_rec_on_id {A : Type} {a : A} {B : A → Type} (H : a = a) (b : B a) : eq_rec_on H b = b :=
 refl (eq_rec_on rfl b)
 
-theorem eq_rec_id {A : Type} {a : A} {B : A → Type} (H : a = a) (b : B a) : eq_rec b H = b :=
+theorem eq_rec_id {A : Type} {a : A} {B : A → Type} (H : a = a) (b : B a) : eq.rec b H = b :=
 eq_rec_on_id H b
 
 theorem eq_rec_on_compose {A : Type} {a b c : A} {P : A → Type} (H1 : a = b) (H2 : b = c)
diff --git a/library/logic/core/if.lean b/library/logic/core/if.lean
index 75aa8390c9..d9a68166fd 100644
--- a/library/logic/core/if.lean
+++ b/library/logic/core/if.lean
@@ -13,19 +13,19 @@ decidable.rec_on H (assume Hc,  t) (assume Hnc, e)
 notation `if` c `then` t `else` e:45 := ite c t e
 
 theorem if_pos {c : Prop} {H : decidable c} (Hc : c) {A : Type} {t e : A} : (if c then t else e) = t :=
-decidable_rec
+decidable.rec
   (assume Hc : c,    refl (@ite c (inl Hc) A t e))
   (assume Hnc : ¬c,  absurd Hc Hnc)
   H
 
 theorem if_neg {c : Prop} {H : decidable c} (Hnc : ¬c) {A : Type} {t e : A} : (if c then t else e) = e :=
-decidable_rec
+decidable.rec
   (assume Hc : c,    absurd Hc Hnc)
   (assume Hnc : ¬c,  refl (@ite c (inr Hnc) A t e))
   H
 
 theorem if_t_t (c : Prop) {H : decidable c} {A : Type} (t : A) : (if c then t else t) = t :=
-decidable_rec
+decidable.rec
   (assume Hc  : c,  refl (@ite c (inl Hc)  A t t))
   (assume Hnc : ¬c, refl (@ite c (inr Hnc) A t t))
   H
diff --git a/library/logic/core/prop.lean b/library/logic/core/prop.lean
index e17f7db63d..c2f45043a2 100644
--- a/library/logic/core/prop.lean
+++ b/library/logic/core/prop.lean
@@ -19,7 +19,7 @@ abbreviation imp (a b : Prop) : Prop := a → b
 inductive false : Prop
 
 theorem false_elim {c : Prop} (H : false) : c :=
-false_rec c H
+false.rec c H
 
 inductive true : Prop :=
 trivial : true
diff --git a/library/logic/core/quantifiers.lean b/library/logic/core/quantifiers.lean
index 8cce880692..1fe15f406a 100644
--- a/library/logic/core/quantifiers.lean
+++ b/library/logic/core/quantifiers.lean
@@ -13,7 +13,7 @@ notation `exists` binders `,` r:(scoped P, Exists P) := r
 notation `∃` binders `,` r:(scoped P, Exists P) := r
 
 theorem exists_elim {A : Type} {p : A → Prop} {B : Prop} (H1 : ∃x, p x) (H2 : ∀ (a : A) (H : p a), B) : B :=
-Exists_rec H2 H1
+Exists.rec H2 H1
 
 theorem exists_not_forall {A : Type} {p : A → Prop} (H : ∃x, p x) : ¬∀x, ¬p x :=
 assume H1 : ∀x, ¬p x,
diff --git a/library/struc/relation.lean b/library/struc/relation.lean
index 6eeca6b8ba..c32ecdb539 100644
--- a/library/struc/relation.lean
+++ b/library/struc/relation.lean
@@ -24,10 +24,10 @@ is_reflexive_mk : reflexive R → is_reflexive R
 namespace is_reflexive
 
   abbreviation app ⦃T : Type⦄ {R : T → T → Type} (C : is_reflexive R) : reflexive R :=
-  is_reflexive_rec (λu, u) C
+  is_reflexive.rec (λu, u) C
 
   abbreviation infer ⦃T : Type⦄ (R : T → T → Type) {C : is_reflexive R} : reflexive R :=
-  is_reflexive_rec (λu, u) C
+  is_reflexive.rec (λu, u) C
 
 end is_reflexive
 
@@ -38,10 +38,10 @@ is_symmetric_mk : symmetric R → is_symmetric R
 namespace is_symmetric
 
   abbreviation app ⦃T : Type⦄ {R : T → T → Type} (C : is_symmetric R) : symmetric R :=
-  is_symmetric_rec (λu, u) C
+  is_symmetric.rec (λu, u) C
 
   abbreviation infer ⦃T : Type⦄ (R : T → T → Type) {C : is_symmetric R} : symmetric R :=
-  is_symmetric_rec (λu, u) C
+  is_symmetric.rec (λu, u) C
 
 end is_symmetric
 
@@ -52,10 +52,10 @@ is_transitive_mk : transitive R → is_transitive R
 namespace is_transitive
 
   abbreviation app ⦃T : Type⦄ {R : T → T → Type} (C : is_transitive R) : transitive R :=
-  is_transitive_rec (λu, u) C
+  is_transitive.rec (λu, u) C
 
   abbreviation infer ⦃T : Type⦄ (R : T → T → Type) {C : is_transitive R} : transitive R :=
-  is_transitive_rec (λu, u) C
+  is_transitive.rec (λu, u) C
 
 end is_transitive
 
@@ -66,13 +66,13 @@ is_equivalence_mk : is_reflexive R → is_symmetric R → is_transitive R → is
 namespace is_equivalence
 
   theorem is_reflexive {T : Type} (R : T → T → Type) {C : is_equivalence R} : is_reflexive R :=
-  is_equivalence_rec (λx y z, x) C
+  is_equivalence.rec (λx y z, x) C
 
   theorem is_symmetric {T : Type} {R : T → T → Type} {C : is_equivalence R} : is_symmetric R :=
-  is_equivalence_rec (λx y z, y) C
+  is_equivalence.rec (λx y z, y) C
 
   theorem is_transitive {T : Type} {R : T → T → Type} {C : is_equivalence R} : is_transitive R :=
-  is_equivalence_rec (λx y z, z) C
+  is_equivalence.rec (λx y z, z) C
 
 end is_equivalence
 
@@ -88,10 +88,10 @@ is_PER_mk : is_symmetric R → is_transitive R → is_PER R
 namespace is_PER
 
   theorem is_symmetric {T : Type} {R : T → T → Type} {C : is_PER R} : is_symmetric R :=
-  is_PER_rec (λx y, x) C
+  is_PER.rec (λx y, x) C
 
   theorem is_transitive {T : Type} {R : T → T → Type} {C : is_PER R} : is_transitive R :=
-  is_PER_rec (λx y, y) C
+  is_PER.rec (λx y, y) C
 
 end is_PER
 
@@ -116,17 +116,17 @@ namespace congruence
 
   abbreviation app {T1 : Type} {R1 : T1 → T1 → Prop} {T2 : Type} {R2 : T2 → T2 → Prop}
       {f : T1 → T2} (C : congruence R1 R2 f) ⦃x y : T1⦄ : R1 x y → R2 (f x) (f y) :=
-  congruence_rec (λu, u) C x y
+  congruence.rec (λu, u) C x y
 
   theorem infer {T1 : Type} (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop)
       (f : T1 → T2) {C : congruence R1 R2 f} ⦃x y : T1⦄ : R1 x y → R2 (f x) (f y) :=
-  congruence_rec (λu, u) C x y
+  congruence.rec (λu, u) C x y
 
   abbreviation app2 {T1 : Type} {R1 : T1 → T1 → Prop} {T2 : Type} {R2 : T2 → T2 → Prop}
       {T3 : Type} {R3 : T3 → T3 → Prop}
       {f : T1 → T2 → T3} (C : congruence2 R1 R2 R3 f) ⦃x1 y1 : T1⦄ ⦃x2 y2 : T2⦄ :
     R1 x1 y1 → R2 x2 y2 → R3 (f x1 x2) (f y1 y2) :=
-  congruence2_rec (λu, u) C x1 y1 x2 y2
+  congruence2.rec (λu, u) C x1 y1 x2 y2
 
 -- ### general tools to build instances
 
@@ -179,10 +179,10 @@ mp_like_mk {} : (a → b) → @mp_like R a b H
 namespace mp_like
 
   definition app {R : Type → Type → Prop} {a : Type} {b : Type} {H : R a b}
-    (C : mp_like H) : a → b := mp_like_rec (λx, x) C
+    (C : mp_like H) : a → b := mp_like.rec (λx, x) C
 
   definition infer ⦃R : Type → Type → Prop⦄ {a : Type} {b : Type} (H : R a b)
-    {C : mp_like H} : a → b := mp_like_rec (λx, x) C
+    {C : mp_like H} : a → b := mp_like.rec (λx, x) C
 
 end mp_like
 
diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp
index c97268adb4..4b6675a65b 100644
--- a/src/frontends/lean/inductive_cmd.cpp
+++ b/src/frontends/lean/inductive_cmd.cpp
@@ -17,6 +17,7 @@ Author: Leonardo de Moura
 #include "library/locals.h"
 #include "library/placeholder.h"
 #include "library/aliases.h"
+#include "library/protected.h"
 #include "library/explicit.h"
 #include "library/opaque_hints.h"
 #include "frontends/lean/decl_cmds.h"
@@ -92,7 +93,7 @@ struct inductive_cmd_fn {
     [[ noreturn ]] void throw_error(sstream const & strm) { throw parser_error(strm, m_pos); }
 
     name mk_rec_name(name const & n) {
-        return n.append_after("_rec");
+        return n + name("rec");
     }
 
     /** \brief Parse the name of an inductive datatype or introduction rule,
@@ -529,7 +530,9 @@ struct inductive_cmd_fn {
             name d_name = inductive_decl_name(d);
             name d_short_name(d_name.get_string());
             env = create_alias(env, d_name, section_levels, section_params);
-            env = create_alias(env, mk_rec_name(d_name), section_levels, section_params);
+            name rec_name = mk_rec_name(d_name);
+            env = create_alias(env, rec_name, section_levels, section_params);
+            env = add_protected(env, rec_name);
             for (intro_rule const & ir : inductive_decl_intros(d)) {
                 name ir_name = intro_rule_name(ir);
                 env = create_alias(env, ir_name, section_levels, section_params);
diff --git a/src/kernel/inductive/inductive.cpp b/src/kernel/inductive/inductive.cpp
index 21a66f43bd..eef6d1337b 100644
--- a/src/kernel/inductive/inductive.cpp
+++ b/src/kernel/inductive/inductive.cpp
@@ -600,7 +600,7 @@ struct add_inductive_fn {
     }
 
     /** \brief Return the name of the eliminator/recursor for \c d. */
-    name get_elim_name(inductive_decl const & d) { return inductive_decl_name(d).append_after("_rec"); }
+    name get_elim_name(inductive_decl const & d) { return inductive_decl_name(d) + name("rec"); }
 
     name get_elim_name(unsigned d_idx) { return get_elim_name(get_ith(m_decls, d_idx)); }
 
diff --git a/tests/lean/interactive/t4.input.expected.out b/tests/lean/interactive/t4.input.expected.out
index 3538a731ba..1eda2f5af8 100644
--- a/tests/lean/interactive/t4.input.expected.out
+++ b/tests/lean/interactive/t4.input.expected.out
@@ -15,7 +15,7 @@ epsilon
 Type
 -- ACK
 -- IDENTIFIER|6|21
-nat.nat
+nat
 -- ACK
 -- TYPE|6|26
 Prop
diff --git a/tests/lean/run/algebra1.lean b/tests/lean/run/algebra1.lean
index 40a8d27794..f53850c030 100644
--- a/tests/lean/run/algebra1.lean
+++ b/tests/lean/run/algebra1.lean
@@ -23,12 +23,12 @@ namespace algebra
   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
+  := mul_struct.rec (fun f, f) s a b
 
   infixl `*`:75 := mul
 
   definition add [inline] {A : Type} {s : add_struct A} (a b : A)
-  := add_struct_rec (fun f, f) s a b
+  := add_struct.rec (fun f, f) s a b
 
   infixl `+`:65 := add
 end algebra
@@ -49,7 +49,7 @@ namespace nat
 
   definition to_nat (n : num) : nat
   := #algebra
-    num_rec zero (λ n, pos_num_rec (succ zero) (λ n r, r + r) (λ n r, r + r + succ zero) n) n
+    num.num.rec zero (λ n, num.pos_num.rec (succ zero) (λ n r, r + r) (λ n r, r + r + succ zero) n) n
 end nat
 
 namespace algebra
@@ -58,10 +58,10 @@ namespace semigroup
   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
+  := semigroup_struct.rec (fun f h, f) s a b
 
   definition assoc [inline] {A : Type} (s : semigroup_struct A) : is_assoc (mul s)
-  := semigroup_struct_rec (fun f h, h) s
+  := semigroup_struct.rec (fun f h, h) s
 
   definition is_mul_struct [inline] [instance] (A : Type) (s : semigroup_struct A) : mul_struct A
   := mk_mul_struct (mul s)
@@ -70,10 +70,10 @@ namespace semigroup
   mk_semigroup : Π (A : Type), semigroup_struct A → semigroup
 
   definition carrier [inline] [coercion] (g : semigroup)
-  := semigroup_rec (fun c s, c) g
+  := semigroup.rec (fun c s, c) g
 
   definition is_semigroup [inline] [instance] (g : semigroup) : semigroup_struct (carrier g)
-  := semigroup_rec (fun c s, s) g
+  := semigroup.rec (fun c s, s) g
 end semigroup
 
 namespace monoid
@@ -83,10 +83,10 @@ namespace monoid
   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
+  := monoid_struct.rec (fun mul id a i, mul) s a b
 
   definition assoc [inline] {A : Type} (s : monoid_struct A) : is_assoc (mul s)
-  := monoid_struct_rec (fun mul id a i, a) s
+  := monoid_struct.rec (fun mul id a i, a) s
 
   open semigroup
   definition is_semigroup_struct [inline] [instance] (A : Type) (s : monoid_struct A) : semigroup_struct A
@@ -96,10 +96,10 @@ namespace monoid
   mk_monoid : Π (A : Type), monoid_struct A → monoid
 
   definition carrier [inline] [coercion] (m : monoid)
-  := monoid_rec (fun c s, c) m
+  := monoid.rec (fun c s, c) m
 
   definition is_monoid [inline] [instance] (m : monoid) : monoid_struct (carrier m)
-  := monoid_rec (fun c s, s) m
+  := monoid.rec (fun c s, s) m
 end monoid
 end algebra
 
diff --git a/tests/lean/run/class4.lean b/tests/lean/run/class4.lean
index 39f59eacbf..be6e7e412e 100644
--- a/tests/lean/run/class4.lean
+++ b/tests/lean/run/class4.lean
@@ -5,7 +5,7 @@ zero : nat,
 succ : nat → nat
 
 definition add (x y : nat)
-:= nat_rec x (λ n r, succ r) y
+:= nat.rec x (λ n r, succ r) y
 
 infixl `+`:65 := add
 
@@ -16,7 +16,7 @@ theorem add_succ_left (x y : nat) : x + (succ y) = succ (x + y)
 := refl _
 
 definition is_zero (x : nat)
-:= nat_rec true (λ n r, false) x
+:= nat.rec true (λ n r, false) x
 
 theorem is_zero_zero : is_zero zero
 := eq_true_elim (refl _)
@@ -25,7 +25,7 @@ theorem not_is_zero_succ (x : nat) : ¬ is_zero (succ x)
 := eq_false_elim (refl _)
 
 theorem dichotomy (m : nat) : m = zero ∨ (∃ n, m = succ n)
-:= nat_rec
+:= nat.rec
      (or_intro_left _ (refl zero))
      (λ m H, or_intro_right _ (exists_intro m (refl (succ m))))
      m
@@ -57,7 +57,7 @@ inductive not_zero (x : nat) : Prop :=
 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
+:= not_zero.rec (λ H1, H1) H
 
 theorem not_zero_add_right [instance] (x y : nat) (H : not_zero y) : not_zero (x + y)
 := not_zero_intro (not_zero_add x y (not_zero_not_is_zero H))
diff --git a/tests/lean/run/class5.lean b/tests/lean/run/class5.lean
index bd16d2d117..5be795e132 100644
--- a/tests/lean/run/class5.lean
+++ b/tests/lean/run/class5.lean
@@ -5,7 +5,7 @@ namespace algebra
   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
+  := mul_struct.rec (λ f, f) s a b
 
   infixl `*`:75 := mul
 end algebra
diff --git a/tests/lean/run/class7.lean b/tests/lean/run/class7.lean
index a77db343b1..0d36c6f11f 100644
--- a/tests/lean/run/class7.lean
+++ b/tests/lean/run/class7.lean
@@ -10,7 +10,7 @@ theorem inh_bool [instance] : inh Prop
 := inh_intro true
 
 theorem inh_fun [instance] {A B : Type} (H : inh B) : inh (A → B)
-:= inh_rec (λ b, inh_intro (λ a : A, b)) H
+:= inh.rec (λ b, inh_intro (λ a : A, b)) H
 
 definition assump := eassumption; now
 
diff --git a/tests/lean/run/class8.lean b/tests/lean/run/class8.lean
index 2716a54ef9..fa75573b42 100644
--- a/tests/lean/run/class8.lean
+++ b/tests/lean/run/class8.lean
@@ -7,7 +7,7 @@ inh_intro : A -> inh A
 instance inh_intro
 
 theorem inh_elim {A : Type} {B : Prop} (H1 : inh A) (H2 : A → B) : B
-:= inh_rec H2 H1
+:= inh.rec H2 H1
 
 theorem inh_exists [instance] {A : Type} {P : A → Prop} (H : ∃x, P x) : inh A
 := obtain w Hw, from H, inh_intro w
@@ -16,7 +16,7 @@ theorem inh_bool [instance] : inh Prop
 := inh_intro true
 
 theorem inh_fun [instance] {A B : Type} (H : inh B) : inh (A → B)
-:= inh_rec (λb, inh_intro (λa : A, b)) H
+:= inh.rec (λb, inh_intro (λa : A, b)) H
 
 theorem pair_inh [instance] {A : Type} {B : Type} (H1 : inh A) (H2 : inh B) : inh (prod A B)
 := inh_elim H1 (λa, inh_elim H2 (λb, inh_intro (pair a b)))
diff --git a/tests/lean/run/class_coe.lean b/tests/lean/run/class_coe.lean
index bcdf5e155e..cdb7ea140e 100644
--- a/tests/lean/run/class_coe.lean
+++ b/tests/lean/run/class_coe.lean
@@ -10,7 +10,7 @@ inductive add_struct (A : Type) :=
 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
+add_struct.rec (λ m, m) S a b
 
 infixl `+`:65 := add
 
diff --git a/tests/lean/run/cody1.lean b/tests/lean/run/cody1.lean
index e72c41f58e..e0ecee89b0 100644
--- a/tests/lean/run/cody1.lean
+++ b/tests/lean/run/cody1.lean
@@ -20,6 +20,6 @@ notation `δ` := delta.
 theorem false_aux : ¬ (δ (i delta))
          := assume H : δ (i delta),
             have H' : r (i delta) (i delta),
-              from eq_rec H (symm retract),
+              from eq.rec H (symm retract),
             H H'.
 end
diff --git a/tests/lean/run/coe2.lean b/tests/lean/run/coe2.lean
index 7cd0e1eadf..8713dc2439 100644
--- a/tests/lean/run/coe2.lean
+++ b/tests/lean/run/coe2.lean
@@ -5,10 +5,10 @@ namespace setoid
   mk_setoid: Π (A : Type), (A → A → Prop) → setoid
 
   definition carrier (s : setoid)
-  := setoid_rec (λ a eq, a) s
+  := setoid.rec (λ a eq, a) s
 
   definition eqv {s : setoid} : carrier s → carrier s → Prop
-  := setoid_rec (λ a eqv, eqv) s
+  := setoid.rec (λ a eqv, eqv) s
 
   infix `≈`:50 := eqv
 
@@ -17,4 +17,4 @@ namespace setoid
   inductive morphism (s1 s2 : setoid) : Type :=
   mk_morphism : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism s1 s2
 
-end setoid
\ No newline at end of file
+end setoid
diff --git a/tests/lean/run/coe3.lean b/tests/lean/run/coe3.lean
index b821c290f1..c9c180e588 100644
--- a/tests/lean/run/coe3.lean
+++ b/tests/lean/run/coe3.lean
@@ -5,10 +5,10 @@ namespace setoid
   mk_setoid: Π (A : Type), (A → A → Prop) → setoid
 
   definition carrier (s : setoid)
-  := setoid_rec (λ a eq, a) s
+  := setoid.rec (λ a eq, a) s
 
   definition eqv {s : setoid} : carrier s → carrier s → Prop
-  := setoid_rec (λ a eqv, eqv) s
+  := setoid.rec (λ a eqv, eqv) s
 
   infix `≈`:50 := eqv
 
@@ -27,4 +27,4 @@ namespace setoid
   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
+end setoid
diff --git a/tests/lean/run/coe4.lean b/tests/lean/run/coe4.lean
index 89f7002939..a1c761f96f 100644
--- a/tests/lean/run/coe4.lean
+++ b/tests/lean/run/coe4.lean
@@ -10,10 +10,10 @@ namespace setoid
   definition test : Type.{2} := setoid.{0}
 
   definition carrier (s : setoid)
-  := setoid_rec (λ a eq, a) s
+  := setoid.rec (λ a eq, a) s
 
   definition eqv {s : setoid} : carrier s → carrier s → Prop
-  := setoid_rec (λ a eqv, eqv) s
+  := setoid.rec (λ a eqv, eqv) s
 
   infix `≈`:50 := eqv
 
@@ -31,4 +31,4 @@ namespace setoid
 
   check morphism2
   check mk_morphism2
-end setoid
\ No newline at end of file
+end setoid
diff --git a/tests/lean/run/coe5.lean b/tests/lean/run/coe5.lean
index 8e5a90ea36..0107967e1f 100644
--- a/tests/lean/run/coe5.lean
+++ b/tests/lean/run/coe5.lean
@@ -10,10 +10,10 @@ namespace setoid
   definition test : Type.{2} := setoid.{0}
 
   definition carrier (s : setoid)
-  := setoid_rec (λ a eq, a) s
+  := setoid.rec (λ a eq, a) s
 
   definition eqv {s : setoid} : carrier s → carrier s → Prop
-  := setoid_rec (λ a eqv, eqv) s
+  := setoid.rec (λ a eqv, eqv) s
 
   infix `≈`:50 := eqv
 
@@ -37,4 +37,4 @@ namespace setoid
 
   check my_struct
   definition tst2 : Type.{4} := my_struct.{1 2 1 2}
-end setoid
\ No newline at end of file
+end setoid
diff --git a/tests/lean/run/coercion_bug2.lean b/tests/lean/run/coercion_bug2.lean
index d350ff743a..758e4dc30e 100644
--- a/tests/lean/run/coercion_bug2.lean
+++ b/tests/lean/run/coercion_bug2.lean
@@ -5,6 +5,6 @@ inductive list (T : Type) : Type :=
 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)
+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 0c6c9322ef..7c67cfc7bd 100644
--- a/tests/lean/run/congr_imp_bug.lean
+++ b/tests/lean/run/congr_imp_bug.lean
@@ -14,7 +14,7 @@ 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) :=
-struc_rec id C x y
+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 :=
@@ -25,7 +25,7 @@ abbreviation app2 {T1 : Type} {T2 : Type} {T3 : Type} {R1 : T1 → T1 → Prop}
     {R2 : T2 → T2 → Prop} {R3 : T3 → T3 → Prop} {f : T1 → T2 → T3}
     (C : struc2 R1 R2 R3 f) {x1 y1 : T1} {x2 y2 : T2}
   : R1 x1 y1 → R2 x2 y2 → R3 (f x1 x2) (f y1 y2) :=
-struc2_rec id C x1 y1 x2 y2
+struc2.rec id C x1 y1 x2 y2
 
 theorem compose21
     {T2 : Type} {R2 : T2 → T2 → Prop}
diff --git a/tests/lean/run/e14.lean b/tests/lean/run/e14.lean
index d4e22922f8..718715d351 100644
--- a/tests/lean/run/e14.lean
+++ b/tests/lean/run/e14.lean
@@ -21,10 +21,10 @@ check vcons zero vnil
 variable n : nat
 check vcons n vnil
 
-check vector_rec
+check vector.rec
 
 definition vector_to_list {A : Type} {n : nat} (v : vector A n) : list A
-:= vector_rec (@nil A) (fun (n : nat) (a : A) (v : vector A n) (l : list A), cons a l) v
+:= vector.rec (@nil A) (fun (n : nat) (a : A) (v : vector A n) (l : list A), cons a l) v
 
 coercion vector_to_list
 
diff --git a/tests/lean/run/e15.lean b/tests/lean/run/e15.lean
index e31ef27f55..3c5f08315a 100644
--- a/tests/lean/run/e15.lean
+++ b/tests/lean/run/e15.lean
@@ -21,7 +21,7 @@ check vcons zero vnil
 variable n : nat
 check vcons n vnil
 
-check vector_rec
+check vector.rec
 
 definition vector_to_list {A : Type} {n : nat} (v : vector A n) : list A
-:= vector_rec nil (fun (n : nat) (a : A) (v : vector A n) (l : list A), cons a l) v
+:= vector.rec nil (fun (n : nat) (a : A) (v : vector A n) (l : list A), cons a l) v
diff --git a/tests/lean/run/e16.lean b/tests/lean/run/e16.lean
index 00e1e5bbd2..06bfbbeeb8 100644
--- a/tests/lean/run/e16.lean
+++ b/tests/lean/run/e16.lean
@@ -21,7 +21,7 @@ check vcons zero vnil
 variable n : nat
 check vcons n vnil
 
-check vector_rec
+check vector.rec
 
 definition vector_to_list {A : Type} {n : nat} (v : vector A n) : list A
-:= vector_rec nil (fun n a v l, cons a l) v
+:= vector.rec nil (fun n a v l, cons a l) v
diff --git a/tests/lean/run/elab_bug1.lean b/tests/lean/run/elab_bug1.lean
index 78ebc0e45b..76fe338902 100644
--- a/tests/lean/run/elab_bug1.lean
+++ b/tests/lean/run/elab_bug1.lean
@@ -23,7 +23,7 @@ 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)
     (f : T1 → T2) {C : congruence R1 R2 f} {x y : T1} : R1 x y → R2 (f x) (f y) :=
-  congruence_rec id C x y
+  congruence.rec id C x y
 
 
 -- General tools to build instances
@@ -59,7 +59,7 @@ theorem congr_not [instance] (T : Type) (R : T → T → Prop) (f : T → Prop)
 
 theorem subst_iff {T : Type} {R : T → T → Prop} {P : T → Prop} {C : congruence R iff P}
     {a b : T} (H : R a b) (H1 : P a) : P b :=
--- iff_mp_left (congruence_rec id C a b H) H1
+-- iff_mp_left (congruence.rec id C a b H) H1
 iff_elim_left (@congr_app _ _ R iff P C a b H) H1
 
 theorem test2 (a b c d e : Prop) (H1 : a ↔ b) (H2 : a ∨ c → ¬(d → a)) : b ∨ c → ¬(d → b) :=
diff --git a/tests/lean/run/export.lean b/tests/lean/run/export.lean
index ec15162674..623541ac5b 100644
--- a/tests/lean/run/export.lean
+++ b/tests/lean/run/export.lean
@@ -1,18 +1,18 @@
 import data.nat
 
-variables a b : nat.nat
+variables a b : nat
 
 namespace boo
-  export nat
+  export nat (rec add)
   check a + b
   check nat.add
   check boo.add
   check add
 end boo
 
-check boo.nat_rec
+check boo.rec
 
 open boo
 check a + b
-check boo.nat_rec
-check nat_rec
+check boo.rec
+check nat.rec
diff --git a/tests/lean/run/group.lean b/tests/lean/run/group.lean
index 07951788c5..c589513698 100644
--- a/tests/lean/run/group.lean
+++ b/tests/lean/run/group.lean
@@ -20,15 +20,15 @@ inductive group : Type :=
 mk_group : Π (A : Type), group_struct A → group
 
 definition carrier (g : group) : Type
-:= group_rec (λ c s, c) g
+:= group.rec (λ c s, c) g
 
 definition group_to_struct [instance] (g : group) : group_struct (carrier g)
-:= group_rec (λ (A : Type) (s : group_struct A), s) g
+:= group.rec (λ (A : Type) (s : group_struct A), s) g
 
 check group_struct
 
 definition mul [inline] {A : Type} {s : group_struct A} (a b : A) : A
-:= group_struct_rec (λ mul one inv h1 h2 h3, mul) s a b
+:= group_struct.rec (λ mul one inv h1 h2 h3, mul) s a b
 
 infixl `*`:75 := mul
 
diff --git a/tests/lean/run/group2.lean b/tests/lean/run/group2.lean
index f56be8b4fb..4019b3fa2d 100644
--- a/tests/lean/run/group2.lean
+++ b/tests/lean/run/group2.lean
@@ -20,17 +20,17 @@ inductive group : Type :=
 mk_group : Π (A : Type), group_struct A → group
 
 definition carrier (g : group) : Type
-:= group_rec (λ c s, c) g
+:= group.rec (λ c s, c) g
 
 coercion carrier
 
 definition group_to_struct [instance] (g : group) : group_struct (carrier g)
-:= group_rec (λ (A : Type) (s : group_struct A), s) g
+:= group.rec (λ (A : Type) (s : group_struct A), s) g
 
 check group_struct
 
 definition mul [inline] {A : Type} {s : group_struct A} (a b : A) : A
-:= group_struct_rec (λ mul one inv h1 h2 h3, mul) s a b
+:= group_struct.rec (λ mul one inv h1 h2 h3, mul) s a b
 
 infixl `*`:75 := mul
 
diff --git a/tests/lean/run/ind0.lean b/tests/lean/run/ind0.lean
index 95d5c81c3d..cc56f124d0 100644
--- a/tests/lean/run/ind0.lean
+++ b/tests/lean/run/ind0.lean
@@ -3,4 +3,4 @@ zero : nat,
 succ : nat → nat
 
 check nat
-check nat_rec.{1}
\ No newline at end of file
+check nat.rec.{1}
diff --git a/tests/lean/run/ind1.lean b/tests/lean/run/ind1.lean
index b67940d6ed..bb53c11719 100644
--- a/tests/lean/run/ind1.lean
+++ b/tests/lean/run/ind1.lean
@@ -4,4 +4,4 @@ cons : A → list A → list A
 
 check list.{1}
 check cons.{1}
-check list_rec.{1 1}
\ No newline at end of file
+check list.rec.{1 1}
diff --git a/tests/lean/run/ind2.lean b/tests/lean/run/ind2.lean
index 927f671735..94b3685252 100644
--- a/tests/lean/run/ind2.lean
+++ b/tests/lean/run/ind2.lean
@@ -9,4 +9,4 @@ vcons : Π {n : nat}, A → vector A n → vector A (succ n)
 check vector.{1}
 check vnil.{1}
 check vcons.{1}
-check vector_rec.{1 1}
+check vector.rec.{1 1}
diff --git a/tests/lean/run/ind3.lean b/tests/lean/run/ind3.lean
index d2234b2fc9..166a2741de 100644
--- a/tests/lean/run/ind3.lean
+++ b/tests/lean/run/ind3.lean
@@ -6,8 +6,8 @@ cons : tree A → forest A → forest A
 
 check tree.{1}
 check forest.{1}
-check tree_rec.{1 1}
-check forest_rec.{1 1}
+check tree.rec.{1 1}
+check forest.rec.{1 1}
 
 print "==============="
 
@@ -16,4 +16,4 @@ mk_group : Π (carrier : Type) (mul : carrier → carrier → carrier) (one : ca
 
 check group.{1}
 check group.{2}
-check group_rec.{1 1}
+check group.rec.{1 1}
diff --git a/tests/lean/run/ind5.lean b/tests/lean/run/ind5.lean
index 57e3962d86..6316907c17 100644
--- a/tests/lean/run/ind5.lean
+++ b/tests/lean/run/ind5.lean
@@ -6,4 +6,4 @@ or_intro_right : B → or A B
 
 check or
 check or_intro_left
-check or_rec
\ No newline at end of file
+check or.rec
diff --git a/tests/lean/run/ind6.lean b/tests/lean/run/ind6.lean
index 95eec64af3..7129f7bdc3 100644
--- a/tests/lean/run/ind6.lean
+++ b/tests/lean/run/ind6.lean
@@ -6,5 +6,5 @@ cons : tree.{u} A → forest.{u} A → forest.{u} A
 
 check tree.{1}
 check forest.{1}
-check tree_rec.{1 1}
-check forest_rec.{1 1}
+check tree.rec.{1 1}
+check forest.rec.{1 1}
diff --git a/tests/lean/run/ind7.lean b/tests/lean/run/ind7.lean
index 8110d609ea..d6cfa6c20e 100644
--- a/tests/lean/run/ind7.lean
+++ b/tests/lean/run/ind7.lean
@@ -5,7 +5,7 @@ namespace list
 
   check list.{1}
   check cons.{1}
-  check list_rec.{1 1}
+  check list.rec.{1 1}
 end list
 
 check list.list.{1}
diff --git a/tests/lean/run/is_nil.lean b/tests/lean/run/is_nil.lean
index 6958798427..e9f9b4898d 100644
--- a/tests/lean/run/is_nil.lean
+++ b/tests/lean/run/is_nil.lean
@@ -6,7 +6,7 @@ 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
+:= list.rec true (fun h t r, false) l
 
 theorem is_nil_nil (A : Type) : is_nil (@nil A)
 := eq_true_elim (refl true)
diff --git a/tests/lean/run/list_elab1.lean b/tests/lean/run/list_elab1.lean
index 6389506e01..07e2a16cd5 100644
--- a/tests/lean/run/list_elab1.lean
+++ b/tests/lean/run/list_elab1.lean
@@ -17,10 +17,10 @@ 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 :=
-list_rec Hnil Hind l
+list.rec Hnil Hind l
 
 definition concat {T : Type} (s t : list T) : list T :=
-list_rec t (fun x : T, fun l : list T, fun u : list T, cons x u) s
+list.rec t (fun x : T, fun l : list T, fun u : list T, cons x u) s
 
 theorem concat_nil {T : Type} (t : list T) : concat t nil = t :=
 list_induction_on t (refl (concat nil nil))
diff --git a/tests/lean/run/match1.lean b/tests/lean/run/match1.lean
index ff1110a11e..0dc67b2e91 100644
--- a/tests/lean/run/match1.lean
+++ b/tests/lean/run/match1.lean
@@ -23,6 +23,6 @@ end
 local f    = Const("f")
 local two1 = Const("two1")
 local two2 = Const("two2")
-local succ = Const({"nat", "succ"})
+local succ = Const({"succ"})
 tst_match(f(succ(mk_var(0)), two1), f(two2, two2))
 *)
diff --git a/tests/lean/run/matrix.lean b/tests/lean/run/matrix.lean
index 2cdcac4f72..f7fe6c1399 100644
--- a/tests/lean/run/matrix.lean
+++ b/tests/lean/run/matrix.lean
@@ -11,9 +11,9 @@ theorem same_dim_eq_args {A : Type} {m1 m2 m1' m2' : matrix A} (H1 : m1 = m1') (
 subst H1 (subst H2 H)
 
 theorem add_congr {A : Type} (m1 m2 m1' m2' : matrix A) (H1 : m1 = m1') (H2 : m2 = m2') (H : same_dim m1 m2) : @add A m1 m2 H = @add A m1' m2' (same_dim_eq_args H1 H2 H) :=
-have base : ∀ (H1 : m1 = m1) (H2 : m2 = m2), @add A m1 m2 H = @add A m1 m2 (eq_rec (eq_rec H H1) H2), from
+have base : ∀ (H1 : m1 = m1) (H2 : m2 = m2), @add A m1 m2 H = @add A m1 m2 (eq.rec (eq.rec H H1) H2), from
   assume H1 H2, rfl,
-have general : ∀ (H1 : m1 = m1') (H2 : m2 = m2'), @add A m1 m2 H = @add A m1' m2' (eq_rec (eq_rec H H1) H2), from
+have general : ∀ (H1 : m1 = m1') (H2 : m2 = m2'), @add A m1 m2 H = @add A m1' m2' (eq.rec (eq.rec H H1) H2), from
   subst H1 (subst H2 base),
-calc @add A m1 m2 H = @add A m1' m2' (eq_rec (eq_rec H H1) H2)  : general H1 H2
+calc @add A m1 m2 H = @add A m1' m2' (eq.rec (eq.rec H H1) H2)  : general H1 H2
             ...     = @add A m1' m2' (same_dim_eq_args H1 H2 H) : same_dim_irrel
diff --git a/tests/lean/run/matrix2.lean b/tests/lean/run/matrix2.lean
index aa615374f0..b6a8f2842a 100644
--- a/tests/lean/run/matrix2.lean
+++ b/tests/lean/run/matrix2.lean
@@ -8,8 +8,8 @@ theorem same_dim_eq_args {A : Type} {m1 m2 m1' m2' : matrix A} (H1 : m1 = m1') (
 subst H1 (subst H2 H)
 
 theorem add_congr {A : Type} (m1 m2 m1' m2' : matrix A) (H1 : m1 = m1') (H2 : m2 = m2') (H : same_dim m1 m2) : @add A m1 m2 H = @add A m1' m2' (same_dim_eq_args H1 H2 H) :=
-have base : ∀ (H1 : m1 = m1) (H2 : m2 = m2), @add A m1 m2 H = @add A m1 m2 (eq_rec (eq_rec H H1) H2), from
+have base : ∀ (H1 : m1 = m1) (H2 : m2 = m2), @add A m1 m2 H = @add A m1 m2 (eq.rec (eq.rec H H1) H2), from
   assume H1 H2, rfl,
-have general : ∀ (H1 : m1 = m1') (H2 : m2 = m2'), @add A m1 m2 H = @add A m1' m2' (eq_rec (eq_rec H H1) H2), from
+have general : ∀ (H1 : m1 = m1') (H2 : m2 = m2'), @add A m1 m2 H = @add A m1' m2' (eq.rec (eq.rec H H1) H2), from
   subst H1 (subst H2 base),
 general H1 H2
diff --git a/tests/lean/run/nat_bug.lean b/tests/lean/run/nat_bug.lean
index 5716c36136..1dcf118290 100644
--- a/tests/lean/run/nat_bug.lean
+++ b/tests/lean/run/nat_bug.lean
@@ -6,9 +6,9 @@ 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
+:= nat.rec H1 H2 a
 
-definition pred (n : nat) := nat_rec zero (fun m x, m) n
+definition pred (n : nat) := nat.rec zero (fun m x, m) n
 theorem pred_zero : pred zero = zero := refl _
 theorem pred_succ (n : nat) : pred (succ n) = n := refl _
 
diff --git a/tests/lean/run/nat_bug2.lean b/tests/lean/run/nat_bug2.lean
index 456c6da7a4..b8ea09247d 100644
--- a/tests/lean/run/nat_bug2.lean
+++ b/tests/lean/run/nat_bug2.lean
@@ -6,9 +6,9 @@ zero : nat,
 succ : nat → nat
 
 abbreviation plus (x y : nat) : nat
-:= nat_rec x (λn r, succ r) y
+:= nat.rec x (λn r, succ r) y
 definition to_nat [coercion] [inline] (n : num) : nat
-:= num_rec zero (λn, pos_num_rec (succ zero) (λn r, plus r (plus r (succ zero))) (λn r, plus r r) n) n
+:= num.num.rec zero (λn, num.pos_num.rec (succ zero) (λn r, plus r (plus r (succ zero))) (λn r, plus r r) n) n
 definition add (x y : nat) : nat
 := plus x y
 variable le : nat → nat → Prop
diff --git a/tests/lean/run/nat_bug3.lean b/tests/lean/run/nat_bug3.lean
index 0282d8d821..9a9bac47bc 100644
--- a/tests/lean/run/nat_bug3.lean
+++ b/tests/lean/run/nat_bug3.lean
@@ -6,9 +6,9 @@ zero : nat,
 succ : nat → nat
 
 abbreviation plus (x y : nat) : nat
-:= nat_rec x (λn r, succ r) y
+:= nat.rec x (λn r, succ r) y
 definition to_nat [coercion] [inline] (n : num) : nat
-:= num_rec zero (λn, pos_num_rec (succ zero) (λn r, plus r (plus r (succ zero))) (λn r, plus r r) n) n
+:= num.num.rec zero (λn, num.pos_num.rec (succ zero) (λn r, plus r (plus r (succ zero))) (λn r, plus r r) n) n
 definition add (x y : nat) : nat
 := plus x y
 variable le : nat → nat → Prop
diff --git a/tests/lean/run/nat_bug4.lean b/tests/lean/run/nat_bug4.lean
index 9a94a2cfa3..1db03ce5da 100644
--- a/tests/lean/run/nat_bug4.lean
+++ b/tests/lean/run/nat_bug4.lean
@@ -5,9 +5,9 @@ inductive nat : Type :=
 zero : nat,
 succ : nat → nat
 
-definition add (x y : nat) : nat := nat_rec x (λn r, succ r) y
+definition add (x y : nat) : nat := nat.rec x (λn r, succ r) y
 infixl `+`:65 := add
-definition mul (n m : nat) := nat_rec zero (fun m x, x + n) m
+definition mul (n m : nat) := nat.rec zero (fun m x, x + n) m
 infixl `*`:75 := mul
 
 axiom mul_succ_right (n m : nat) : n * succ m = n * m + n
diff --git a/tests/lean/run/nat_bug5.lean b/tests/lean/run/nat_bug5.lean
index e172cc3d84..69cdca9c6b 100644
--- a/tests/lean/run/nat_bug5.lean
+++ b/tests/lean/run/nat_bug5.lean
@@ -5,9 +5,9 @@ inductive nat : Type :=
 zero : nat,
 succ : nat → nat
 
-definition add (x y : nat) : nat := nat_rec x (λn r, succ r) y
+definition add (x y : nat) : nat := nat.rec x (λn r, succ r) y
 infixl `+`:65 := add
-definition mul (n m : nat) := nat_rec zero (fun m x, x + n) m
+definition mul (n m : nat) := nat.rec zero (fun m x, x + n) m
 infixl `*`:75 := mul
 
 axiom add_one (n:nat) : n + (succ zero) = succ n
diff --git a/tests/lean/run/nat_bug6.lean b/tests/lean/run/nat_bug6.lean
index 9be8a1ffc7..b8669f59bc 100644
--- a/tests/lean/run/nat_bug6.lean
+++ b/tests/lean/run/nat_bug6.lean
@@ -5,9 +5,9 @@ inductive nat : Type :=
 zero : nat,
 succ : nat → nat
 
-definition add (x y : nat) : nat := nat_rec x (λn r, succ r) y
+definition add (x y : nat) : nat := nat.rec x (λn r, succ r) y
 infixl `+`:65 := add
-definition mul (n m : nat) := nat_rec zero (fun m x, x + n) m
+definition mul (n m : nat) := nat.rec zero (fun m x, x + n) m
 infixl `*`:75 := mul
 
 axiom mul_zero_right (n : nat) : n * zero = zero
diff --git a/tests/lean/run/nat_bug7.lean b/tests/lean/run/nat_bug7.lean
index 4cbd261240..ed6318f61d 100644
--- a/tests/lean/run/nat_bug7.lean
+++ b/tests/lean/run/nat_bug7.lean
@@ -4,7 +4,7 @@ inductive nat : Type :=
 zero : nat,
 succ : nat → nat
 
-definition add (x y : nat) : nat := nat_rec x (λn r, succ r) y
+definition add (x y : nat) : nat := nat.rec x (λn r, succ r) y
 infixl `+`:65 := add
 
 axiom add_right_comm (n m k : nat) : n + m + k = n + k + m
diff --git a/tests/lean/run/opaque_hint_bug.lean b/tests/lean/run/opaque_hint_bug.lean
index d6de03b4b3..24349158f2 100644
--- a/tests/lean/run/opaque_hint_bug.lean
+++ b/tests/lean/run/opaque_hint_bug.lean
@@ -7,8 +7,8 @@ section
   variable {T : Type}
 
   definition concat (s t : list T) : list T
-  := list_rec t (fun x l u, cons x u) s
+  := list.rec t (fun x l u, cons x u) s
 
   opaque_hint (hiding concat)
 
-end
\ No newline at end of file
+end
diff --git a/tests/lean/run/rel.lean b/tests/lean/run/rel.lean
index 8b58b0e9f4..b7569974ba 100644
--- a/tests/lean/run/rel.lean
+++ b/tests/lean/run/rel.lean
@@ -7,13 +7,13 @@ namespace is_equivalence
   mk : is_reflexive R → is_symmetric R → is_transitive R → cls R
 
   theorem is_reflexive {T : Type} {R : T → T → Type} {C : cls R} : is_reflexive R :=
-  cls_rec (λx y z, x) C
+  cls.rec (λx y z, x) C
 
   theorem is_symmetric {T : Type} {R : T → T → Type} {C : cls R} : is_symmetric R :=
-  cls_rec (λx y z, y) C
+  cls.rec (λx y z, y) C
 
   theorem is_transitive {T : Type} {R : T → T → Type} {C : cls R} : is_transitive R :=
-  cls_rec (λx y z, z) C
+  cls.rec (λx y z, z) C
 
 end is_equivalence
 
diff --git a/tests/lean/run/sum_bug.lean b/tests/lean/run/sum_bug.lean
index 09fbc10fb9..e6e15bb678 100644
--- a/tests/lean/run/sum_bug.lean
+++ b/tests/lean/run/sum_bug.lean
@@ -17,7 +17,7 @@ infixr `+`:25 := sum
 
 abbreviation rec_on {A B : Type} {C : (A + B) → Type} (s : A + B)
   (H1 : ∀a : A, C (inl B a)) (H2 : ∀b : B, C (inr A b)) : C s :=
-sum_rec H1 H2 s
+sum.rec H1 H2 s
 
 
 theorem inl_inj {A B : Type} {a1 a2 : A} (H : inl B a1 = inl B a2) : a1 = a2 :=
@@ -28,7 +28,7 @@ H2
 
 abbreviation cases_on {A B : Type} {P : (A + B) → Prop} (s : A + B)
   (H1 : ∀a : A, P (inl B a)) (H2 : ∀b : B, P (inr A b)) : P s :=
-sum_rec H1 H2 s
+sum.rec H1 H2 s
 
 theorem inl_neq_inr {A B : Type} {a : A} {b : B} (H : inl B a = inr A b) : false :=
 let f := λs, rec_on s (λa', a = a') (λb, false) in
diff --git a/tests/lean/run/tactic23.lean b/tests/lean/run/tactic23.lean
index e4064b382c..a9f14f247a 100644
--- a/tests/lean/run/tactic23.lean
+++ b/tests/lean/run/tactic23.lean
@@ -1,5 +1,5 @@
 import logic
-open num (num pos_num num_rec pos_num_rec)
+open num (num pos_num num.rec pos_num.rec)
 open tactic
 
 inductive nat : Type :=
@@ -7,7 +7,7 @@ zero : nat,
 succ : nat → nat
 
 definition add [inline] (a b : nat) : nat
-:= nat_rec a (λ n r, succ r) b
+:= nat.rec a (λ n r, succ r) b
 infixl `+`:65 := add
 
 definition one [inline] := succ zero
@@ -15,9 +15,9 @@ definition one [inline] := succ zero
 -- Define coercion from num -> nat
 -- By default the parser converts numerals into a binary representation num
 definition pos_num_to_nat [inline] (n : pos_num) : nat
-:= pos_num_rec one (λ n r, r + r) (λ n r, r + r + one) n
+:= pos_num.rec one (λ n r, r + r) (λ n r, r + r + one) n
 definition num_to_nat [inline] (n : num) : nat
-:= num_rec zero (λ n, pos_num_to_nat n) n
+:= num.rec zero (λ n, pos_num_to_nat n) n
 coercion num_to_nat
 
 -- Now we can write 2 + 3, the coercion will be applied
@@ -30,7 +30,7 @@ theorem T1 {p : nat → Prop} {a : nat } (H : p (a+2)) : ∃ x, p (succ x)
 := by apply exists_intro; assump
 
 definition is_zero (n : nat)
-:= nat_rec true (λ n r, false) n
+:= nat.rec true (λ n r, false) n
 
 theorem T2 : ∃ a, (is_zero a) = true
 := by apply exists_intro; apply refl
diff --git a/tests/lean/run/tactic26.lean b/tests/lean/run/tactic26.lean
index 3ecad84646..70c72c4b03 100644
--- a/tests/lean/run/tactic26.lean
+++ b/tests/lean/run/tactic26.lean
@@ -1,6 +1,7 @@
 import logic
 open tactic inhabited
 
+namespace foo
 inductive sum (A : Type) (B : Type) : Type :=
 inl  : A → sum A B,
 inr  : B → sum A B
@@ -19,3 +20,5 @@ definition my_tac := fixpoint (λ t, [ apply @inl_inhabited; t
 tactic_hint [inhabited] my_tac
 
 theorem T : inhabited (sum false num.num)
+
+end foo
diff --git a/tests/lean/run/tactic28.lean b/tests/lean/run/tactic28.lean
index 2f29c25514..ebc5df4a8e 100644
--- a/tests/lean/run/tactic28.lean
+++ b/tests/lean/run/tactic28.lean
@@ -1,6 +1,7 @@
 import logic
 open tactic inhabited
 
+namespace foo
 inductive sum (A : Type) (B : Type) : Type :=
 inl  : A → sum A B,
 inr  : B → sum A B
@@ -22,3 +23,5 @@ definition my_tac := repeat (trace "iteration"; state;
 tactic_hint [inhabited] my_tac
 
 theorem T : inhabited (sum false num.num)
+
+end foo
diff --git a/tests/lean/run/trans.lean b/tests/lean/run/trans.lean
index 0ffe9520fe..768dedf130 100644
--- a/tests/lean/run/trans.lean
+++ b/tests/lean/run/trans.lean
@@ -4,7 +4,7 @@
 import logic
 
 definition transport {A : Type} {a b : A} {P : A → Type} (p : a = b) (H : P a) : P b
-:= eq_rec H p
+:= eq.rec H p
 
 theorem transport_refl {A : Type} {a : A} {P : A → Type} (H : P a) : transport (refl a) H = H
 := refl H
@@ -20,12 +20,11 @@ theorem transport_eq {A : Type} {a : A} {P : A → Type} (p : a = a) (H : P a) :
 theorem dcongr {A : Type} {B : A → Type} {a b : A} (f : Π x, B x) (p : a = b) : transport p (f a) = f b
 := have H1 : ∀ p1 : a = a, transport p1 (f a) = f a, from
      assume p1 : a = a, transport_eq p1 (f a),
-   eq_rec H1 p p
+   eq.rec H1 p p
 
 theorem transport_trans {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
                        transport p1 (transport p2 H) = transport (trans p1 p2) H
 := have H1 : ∀ p, transport p1 (transport p H) = transport (trans p1 p) H, from
      take p, calc transport p1 (transport p H) = transport p1 H           : {transport_eq p H}
                                           ...  = transport (trans p1 p) H : refl (transport p1 H),
-   eq_rec H1 p2 p2
-
+   eq.rec H1 p2 p2
diff --git a/tests/lean/run/uni.lean b/tests/lean/run/uni.lean
index 8935b3638f..a02a76f29d 100644
--- a/tests/lean/run/uni.lean
+++ b/tests/lean/run/uni.lean
@@ -4,11 +4,11 @@ inductive nat : Type :=
 zero : nat,
 succ : nat → nat
 
-check @nat_rec
+check @nat.rec
 
 (*
 local env     = get_env()
-local nat_rec = Const("nat_rec", {1})
+local nat_rec = Const({"nat", "rec"}, {1})
 local nat     = Const("nat")
 local n       = Local("n", nat)
 local C       = Fun(n, Prop)
@@ -45,4 +45,4 @@ end
 
 test_unify(env, t(m), tt, 1)
 test_unify(env, t(m), ff, 1)
-*)
\ No newline at end of file
+*)
diff --git a/tests/lean/run/uni2.lean b/tests/lean/run/uni2.lean
index 143189e003..f9527f4f96 100644
--- a/tests/lean/run/uni2.lean
+++ b/tests/lean/run/uni2.lean
@@ -6,11 +6,11 @@ succ : nat → nat
 
 variable f : nat → nat
 
-check @nat_rec
+check @nat.rec
 
 (*
 local env     = get_env()
-local nat_rec = Const("nat_rec", {1})
+local nat_rec = Const({"nat", "rec"}, {1})
 local nat     = Const("nat")
 local f       = Const("f")
 local n       = Local("n", nat)
@@ -47,4 +47,4 @@ function test_unify(env, lhs, rhs, num_s)
 end
 
 test_unify(env, f(t(m)), f(tt), 1)
-*)
\ No newline at end of file
+*)
diff --git a/tests/lean/run/uni_issue1.lean b/tests/lean/run/uni_issue1.lean
index f67c0f1834..adb8ac83c0 100644
--- a/tests/lean/run/uni_issue1.lean
+++ b/tests/lean/run/uni_issue1.lean
@@ -5,4 +5,4 @@ zero : nat,
 succ : nat → nat
 
 definition is_zero (n : nat)
-:= nat_rec true (λ n r, false) n
+:= nat.rec true (λ n r, false) n
diff --git a/tests/lean/run/univ_bug1.lean b/tests/lean/run/univ_bug1.lean
index a0053cb7f4..736c5facdc 100644
--- a/tests/lean/run/univ_bug1.lean
+++ b/tests/lean/run/univ_bug1.lean
@@ -16,10 +16,10 @@ inductive simplifies_to {T : Type} (t1 t2 : T) : Prop :=
 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
+simplifies_to.rec (λx, x) C
 
 theorem infer_eq {T : Type} (t1 t2 : T) {C : simplifies_to t1 t2} : t1 = t2 :=
-simplifies_to_rec (λx, x) C
+simplifies_to.rec (λx, x) C
 
 theorem simp_app [instance] (S T : Type) (f1 f2 : S → T) (s1 s2 : S)
    (C1 : simplifies_to f1 f2) (C2 : simplifies_to s1 s2) : simplifies_to (f1 s1) (f2 s2) :=
diff --git a/tests/lean/run/univ_bug2.lean b/tests/lean/run/univ_bug2.lean
index ad3c6833f1..51f9b06294 100644
--- a/tests/lean/run/univ_bug2.lean
+++ b/tests/lean/run/univ_bug2.lean
@@ -13,10 +13,10 @@ inductive simplifies_to {T : Type} (t1 t2 : T) : Prop :=
 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
+simplifies_to.rec (λx, x) C
 
 theorem infer_eq {T : Type} (t1 t2 : T) {C : simplifies_to t1 t2} : t1 = t2 :=
-simplifies_to_rec (λx, x) C
+simplifies_to.rec (λx, x) C
 
 theorem simp_app [instance] (S : Type) (T : Type) (f1 f2 : S → T) (s1 s2 : S)
    (C1 : simplifies_to f1 f2) (C2 : simplifies_to s1 s2) : simplifies_to (f1 s1) (f2 s2) :=
diff --git a/tests/lean/run/uuu.lean b/tests/lean/run/uuu.lean
index ac8d57c80b..a9dba1d69c 100644
--- a/tests/lean/run/uuu.lean
+++ b/tests/lean/run/uuu.lean
@@ -26,15 +26,15 @@ inductive total2 {T: Type} (P: T → Type) : Type :=
 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
+:= total2.rec (λ a b, a) tp
 definition pr2 {T : Type} {P : T → Type} (tp : total2 P) : P (pr1 tp)
-:= total2_rec (λ a b, b) tp
+:= total2.rec (λ a b, b) tp
 
 inductive Phant (T : Type) : Type :=
 phant : Phant T
 
 definition fromempty {X : Type} : empty → X
-:= λe, empty_rec (λe, X) e
+:= λe, empty.rec (λe, X) e
 
 definition tounit {X : Type} : X → unit
 := λx, tt
@@ -50,7 +50,7 @@ abbreviation funcomp {X : Type} {Y : Type} {Z : Type} (f : X → Y) (g : Y → Z
 infixl `∘`:60 := funcomp
 
 definition iteration {T : Type} (f : T → T) (n : nat) : T → T
-:= nat_rec (idfun T) (λ m fm, funcomp fm f) n
+:= nat.rec (idfun T) (λ m fm, funcomp fm f) n
 
 definition adjev {X : Type} {Y : Type} (x : X) (f : X → Y) := f x
 
@@ -98,16 +98,16 @@ definition logeqnegs {X : Type} {Y : Type} (l : X ↔ Y) : (neg X) ↔ (neg Y)
 infix `=`:50      := paths
 
 definition pathscomp0 {X : Type} {a b c : X} (e1 : a = b) (e2 : b = c) : a = c
-:= paths_rec e1 e2
+:= paths.rec e1 e2
 
 definition pathscomp0rid {X : Type} {a b : X} (e1 : a = b) : pathscomp0 e1 (idpath b) = e1
 := idpath _
 
 definition pathsinv0 {X : Type} {a b : X} (e : a = b) : b = a
-:= paths_rec (idpath _) e
+:= paths.rec (idpath _) e
 
 definition transport {A : Type} {a b : A} {P : A → Type} (H1 : a = b) (H2 : P a) : P b
-:= paths_rec H2 H1
+:= paths.rec H2 H1
 
 infixr `▸`:75     := transport
 infixr `⬝`:75     := pathscomp0
@@ -120,13 +120,13 @@ definition idtrans {A : Type} (x : A) : (idpath x) ⬝ (idpath x) = (idpath x)
 := idpath (idpath x)
 
 definition pathsinv0l {X : Type} {a b : X} (e : a = b) : e⁻¹ ⬝ e = idpath b
-:= paths_rec (idinv a⁻¹ ▸ idtrans a) e
+:= paths.rec (idinv a⁻¹ ▸ idtrans a) e
 
 definition pathsinv0r {A : Type} {x y : A} (p : x = y) : p⁻¹ ⬝ p = idpath y
-:= paths_rec (idinv x⁻¹ ▸ idtrans x) p
+:= paths.rec (idinv x⁻¹ ▸ idtrans x) p
 
 definition pathsinv0inv0 {A : Type} {x y : A} (p : x = y) : (p⁻¹)⁻¹ = p
-:= paths_rec (idpath (idpath x)) p
+:= paths.rec (idpath (idpath x)) p
 
 definition pathsdirprod {X : Type} {Y : Type} {x1 x2 : X} {y1 y2 : Y} (ex : x1 = x2) (ey : y1 = y2 ) : dirprodpair x1 y1 =  dirprodpair x2 y2
 := ex ▸ ey ▸ idpath (dirprodpair x1 y1)
@@ -137,13 +137,13 @@ definition maponpaths {T1 : Type} {T2 : Type} (f : T1 → T2) {t1 t2 : T1} (e :
 definition ap {T1 : Type} {T2 : Type} := @maponpaths T1 T2
 
 definition maponpathscomp0 {X : Type} {Y : Type} {x y z : X} (f : X → Y) (p : x = y) (q : y = z) : ap f (p ⬝ q) = (ap f p) ⬝ (ap f q)
-:= paths_rec (idpath _) q
+:= paths.rec (idpath _) q
 
 definition maponpathsinv0 {X : Type} {Y : Type} (f : X → Y) {x1 x2 : X} (e : x1 = x2 ) : ap f (e⁻¹) = (ap f e)⁻¹
-:= paths_rec (idpath _) e
+:= paths.rec (idpath _) e
 
 lemma maponpathsidfun {X : Type} {x x' : X} (e : x = x') : ap (idfun X) e = e
-:= paths_rec (idpath _) e
+:= paths.rec (idpath _) e
 
 lemma maponpathscomp {X : Type} {Y : Type} {Z : Type} {x x' : X} (f : X → Y) (g : Y → Z) (e : x = x') : ap g (ap f e) = ap (f ∘ g) e
-:= paths_rec (idpath _) e
+:= paths.rec (idpath _) e
diff --git a/tests/lean/slow/list_elab2.lean b/tests/lean/slow/list_elab2.lean
index 1315debd84..aa5817c4a5 100644
--- a/tests/lean/slow/list_elab2.lean
+++ b/tests/lean/slow/list_elab2.lean
@@ -33,7 +33,7 @@ variable {T : Type}
 
 theorem list_induction_on {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 :=
-list_rec Hnil Hind l
+list.rec Hnil Hind l
 
 theorem list_cases_on {P : list T → Prop} (l : list T) (Hnil : P nil)
     (Hcons : forall x : T, forall l : list T, P (cons x l)) : P l :=
@@ -46,7 +46,7 @@ notation `[` l:(foldr `,` (h t, cons h t) nil) `]` := l
 -- ------
 
 definition concat (s t : list T) : list T :=
-list_rec t (fun x : T, fun l : list T, fun u : list T, cons x u) s
+list.rec t (fun x : T, fun l : list T, fun u : list T, cons x u) s
 
 infixl `++` : 65 := concat
 
@@ -97,7 +97,7 @@ list_induction_on s (refl _)
 -- Length
 -- ------
 
-definition length : list T → ℕ := list_rec 0 (fun x l m, succ m)
+definition length : list T → ℕ := list.rec 0 (fun x l m, succ m)
 
 -- TODO: cannot replace zero by 0
 theorem length_nil : length (@nil T) = zero := refl _
@@ -121,7 +121,7 @@ list_induction_on s
 -- Reverse
 -- -------
 
-definition reverse : list T → list T := list_rec nil (fun x l r, r ++ [x])
+definition reverse : list T → list T := list.rec nil (fun x l r, r ++ [x])
 
 theorem reverse_nil : reverse (@nil T) = nil := refl _
 
@@ -159,7 +159,7 @@ list_induction_on l (refl _)
 
 -- TODO: define reverse from append
 
-definition append (x : T) : list T → list T := list_rec (x :: nil) (fun y l l', y :: l')
+definition append (x : T) : list T → list T := list.rec (x :: nil) (fun y l l', y :: l')
 
 theorem append_nil (x : T) : append x nil = [x] := refl _
 
diff --git a/tests/lean/slow/nat_bug1.lean b/tests/lean/slow/nat_bug1.lean
index a571458fe7..c2c1ea9b3c 100644
--- a/tests/lean/slow/nat_bug1.lean
+++ b/tests/lean/slow/nat_bug1.lean
@@ -13,11 +13,11 @@ succ : nat → nat
 notation `ℕ`:max := nat
 
 abbreviation plus (x y : ℕ) : ℕ
-:= nat_rec x (λ n r, succ r) y
+:= nat.rec x (λ n r, succ r) y
 
 definition to_nat [coercion] [inline] (n : num) : ℕ
-:= num_rec zero (λ n, pos_num_rec (succ zero) (λ n r, plus r (plus r (succ zero))) (λ n r, plus r r) n) n
+:= num.num.rec zero (λ n, num.pos_num.rec (succ zero) (λ n r, plus r (plus r (succ zero))) (λ n r, plus r r) n) n
 
 print "=================="
-theorem nat_rec_zero {P : ℕ → Type} (x : P 0) (f : ∀m, P m → P (succ m)) : nat_rec x f 0 = x :=
+theorem nat_rec_zero {P : ℕ → Type} (x : P 0) (f : ∀m, P m → P (succ m)) : nat.rec x f 0 = x :=
 refl _
diff --git a/tests/lean/slow/nat_bug2.lean b/tests/lean/slow/nat_bug2.lean
index 925eeb1645..140a8d2dd9 100644
--- a/tests/lean/slow/nat_bug2.lean
+++ b/tests/lean/slow/nat_bug2.lean
@@ -15,10 +15,10 @@ succ : nat → nat
 notation `ℕ`:max := nat
 
 abbreviation plus (x y : ℕ) : ℕ
-:= nat_rec x (λ n r, succ r) y
+:= nat.rec x (λ n r, succ r) y
 
 definition to_nat [coercion] [inline] (n : num) : ℕ
-:= num_rec zero (λ n, pos_num_rec (succ zero) (λ n r, plus r (plus r (succ zero))) (λ n r, plus r r) n) n
+:= num.num.rec zero (λ n, num.pos_num.rec (succ zero) (λ n r, plus r (plus r (succ zero))) (λ n r, plus r r) n) n
 
 namespace helper_tactics
   definition apply_refl := apply @refl
@@ -26,28 +26,28 @@ namespace helper_tactics
 end helper_tactics
 open helper_tactics
 
-theorem nat_rec_zero {P : ℕ → Type} (x : P 0) (f : ∀m, P m → P (succ m)) : nat_rec x f 0 = x
+theorem nat_rec_zero {P : ℕ → Type} (x : P 0) (f : ∀m, P m → P (succ m)) : nat.rec x f 0 = x
 
-theorem nat_rec_succ {P : ℕ → Type} (x : P 0) (f : ∀m, P m → P (succ m)) (n : ℕ) : nat_rec x f (succ n) = f n (nat_rec x f n)
+theorem nat_rec_succ {P : ℕ → Type} (x : P 0) (f : ∀m, P m → P (succ m)) (n : ℕ) : nat.rec x f (succ n) = f n (nat.rec x f n)
 
 theorem induction_on {P : ℕ → Prop} (a : ℕ) (H1 : P 0) (H2 : ∀ (n : ℕ) (IH : P n), P (succ n)) : P a
-:= nat_rec H1 H2 a
+:= nat.rec H1 H2 a
 
 definition rec_on {P : ℕ → Type} (n : ℕ) (H1 : P 0) (H2 : ∀m, P m → P (succ m)) : P n
-:= nat_rec H1 H2 n
+:= nat.rec H1 H2 n
 
 -------------------------------------------------- succ pred
 
 theorem succ_ne_zero (n : ℕ) : succ n ≠ 0
 := assume H : succ n = 0,
      have H2 : true = false, from
-     let f := (nat_rec false (fun a b, true)) in
+     let f := (nat.rec false (fun a b, true)) in
        calc true = f (succ n) : _
              ... = f 0        : {H}
              ... = false      : _,
      absurd H2 true_ne_false
 
-definition pred (n : ℕ) := nat_rec 0 (fun m x, m) n
+definition pred (n : ℕ) := nat.rec 0 (fun m x, m) n
 
 theorem pred_zero : pred 0 = 0
 
@@ -260,11 +260,11 @@ theorem add_one_left (n:ℕ) : 1 + n = succ n
 --the following theorem has a terrible name, but since the name is not a substring or superstring of another name, it is at least easy to globally replace it
 theorem induction_plus_one {P : ℕ → Prop} (a : ℕ) (H1 : P 0)
     (H2 : ∀ (n : ℕ) (IH : P n), P (n + 1)) : P a
-:= nat_rec H1 (take n IH, (add_one n) ▸ (H2 n IH)) a
+:= nat.rec H1 (take n IH, (add_one n) ▸ (H2 n IH)) a
 
 -------------------------------------------------- mul
 
-definition mul (n m : ℕ) := nat_rec 0 (fun m x, x + n) m
+definition mul (n m : ℕ) := nat.rec 0 (fun m x, x + n) m
 infixl `*`:75 := mul
 
 theorem mul_zero_right (n:ℕ) : n * 0 = 0
@@ -1061,7 +1061,7 @@ theorem mul_eq_one {n m : ℕ} (H : n * m = 1) : n = 1 ∧ m = 1
 
 -------------------------------------------------- sub
 
-definition sub (n m : ℕ) : ℕ := nat_rec n (fun m x, pred x) m
+definition sub (n m : ℕ) : ℕ := nat.rec n (fun m x, pred x) m
 infixl `-`:65 := sub
 theorem sub_zero_right (n : ℕ) : n - 0 = n
 theorem sub_succ_right (n m : ℕ) : n - succ m = pred (n - m)
diff --git a/tests/lean/slow/nat_wo_hints.lean b/tests/lean/slow/nat_wo_hints.lean
index 3a41396366..15c68dd90f 100644
--- a/tests/lean/slow/nat_wo_hints.lean
+++ b/tests/lean/slow/nat_wo_hints.lean
@@ -15,10 +15,10 @@ succ : nat → nat
 notation `ℕ`:max := nat
 
 abbreviation plus (x y : ℕ) : ℕ
-:= nat_rec x (λ n r, succ r) y
+:= nat.rec x (λ n r, succ r) y
 
 definition to_nat [coercion] [inline] (n : num) : ℕ
-:= num_rec zero (λ n, pos_num_rec (succ zero) (λ n r, plus r (plus r (succ zero))) (λ n r, plus r r) n) n
+:= num.num.rec zero (λ n, num.pos_num.rec (succ zero) (λ n r, plus r (plus r (succ zero))) (λ n r, plus r r) n) n
 
 namespace helper_tactics
   definition apply_refl := apply @refl
@@ -26,28 +26,28 @@ namespace helper_tactics
 end helper_tactics
 open helper_tactics
 
-theorem nat_rec_zero {P : ℕ → Type} (x : P 0) (f : ∀m, P m → P (succ m)) : nat_rec x f 0 = x
+theorem nat_rec_zero {P : ℕ → Type} (x : P 0) (f : ∀m, P m → P (succ m)) : nat.rec x f 0 = x
 
-theorem nat_rec_succ {P : ℕ → Type} (x : P 0) (f : ∀m, P m → P (succ m)) (n : ℕ) : nat_rec x f (succ n) = f n (nat_rec x f n)
+theorem nat_rec_succ {P : ℕ → Type} (x : P 0) (f : ∀m, P m → P (succ m)) (n : ℕ) : nat.rec x f (succ n) = f n (nat.rec x f n)
 
 theorem induction_on {P : ℕ → Prop} (a : ℕ) (H1 : P 0) (H2 : ∀ (n : ℕ) (IH : P n), P (succ n)) : P a
-:= nat_rec H1 H2 a
+:= nat.rec H1 H2 a
 
 definition rec_on {P : ℕ → Type} (n : ℕ) (H1 : P 0) (H2 : ∀m, P m → P (succ m)) : P n
-:= nat_rec H1 H2 n
+:= nat.rec H1 H2 n
 
 -------------------------------------------------- succ pred
 
 theorem succ_ne_zero (n : ℕ) : succ n ≠ 0
 := assume H : succ n = 0,
      have H2 : true = false, from
-     let f := (nat_rec false (fun a b, true)) in
+     let f := (nat.rec false (fun a b, true)) in
        calc true = f (succ n) : _
              ... = f 0        : {H}
              ... = false      : _,
      absurd H2 true_ne_false
 
-definition pred (n : ℕ) := nat_rec 0 (fun m x, m) n
+definition pred (n : ℕ) := nat.rec 0 (fun m x, m) n
 
 theorem pred_zero : pred 0 = 0
 
@@ -260,11 +260,11 @@ theorem add_one_left (n:ℕ) : 1 + n = succ n
 --the following theorem has a terrible name, but since the name is not a substring or superstring of another name, it is at least easy to globally replace it
 theorem induction_plus_one {P : ℕ → Prop} (a : ℕ) (H1 : P 0)
     (H2 : ∀ (n : ℕ) (IH : P n), P (n + 1)) : P a
-:= nat_rec H1 (take n IH, (add_one n) ▸ (H2 n IH)) a
+:= nat.rec H1 (take n IH, (add_one n) ▸ (H2 n IH)) a
 
 -------------------------------------------------- mul
 
-definition mul (n m : ℕ) := nat_rec 0 (fun m x, x + n) m
+definition mul (n m : ℕ) := nat.rec 0 (fun m x, x + n) m
 infixl `*`:75 := mul
 
 theorem mul_zero_right (n:ℕ) : n * 0 = 0
@@ -1071,7 +1071,7 @@ theorem mul_eq_one {n m : ℕ} (H : n * m = 1) : n = 1 ∧ m = 1
 
 -------------------------------------------------- sub
 
-definition sub (n m : ℕ) : ℕ := nat_rec n (fun m x, pred x) m
+definition sub (n m : ℕ) : ℕ := nat.rec n (fun m x, pred x) m
 infixl `-`:65 := sub
 theorem sub_zero_right (n : ℕ) : n - 0 = n
 theorem sub_succ_right (n m : ℕ) : n - succ m = pred (n - m)
diff --git a/tests/lean/slow/path_groupoids.lean b/tests/lean/slow/path_groupoids.lean
index 2a5fed8e93..dd7c825542 100644
--- a/tests/lean/slow/path_groupoids.lean
+++ b/tests/lean/slow/path_groupoids.lean
@@ -24,7 +24,7 @@ notation `idp`:max := idpath _     -- TODO: can we / should we use `1`?
 namespace path
   abbreviation induction_on {A : Type} {a b : A} (p : a ≈ b)
     {C : Π (b : A) (p : a ≈ b), Type} (H : C a (idpath a)) : C b p :=
-  path_rec H p
+  path.rec H p
 end path
 
 open path
@@ -33,11 +33,11 @@ open path
 -- -------------------------
 
 definition concat {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : x ≈ z :=
-path_rec (λu, u) q p
+path.rec (λu, u) q p
 
 -- TODO: should this be an abbreviation?
 definition inverse {A : Type} {x y : A} (p : x ≈ y) : y ≈ x :=
-path_rec (idpath x) p
+path.rec (idpath x) p
 
 infixl `@`:75 := concat
 postfix `^`:100 := inverse
diff --git a/tests/lua/ac.lua b/tests/lua/ac.lua
index e236050ecb..e5b7852b26 100644
--- a/tests/lua/ac.lua
+++ b/tests/lua/ac.lua
@@ -14,4 +14,4 @@ function display_type(env, t)
    print(tostring(t) .. " : " .. tostring(type_checker(env):infer(t)))
 end
 
-display_type(env, Const("Acc_rec", {1}))
+display_type(env, Const({"Acc", "rec"}, {1}))
diff --git a/tests/lua/acc.lua b/tests/lua/acc.lua
index 5b0fca43a2..8af444ba44 100644
--- a/tests/lua/acc.lua
+++ b/tests/lua/acc.lua
@@ -20,7 +20,7 @@ env = env:add_universe("u")
 env = env:add_universe("v")
 local u = global_univ("u")
 local v = global_univ("v")
-display_type(env, Const("Acc_rec", {v, u}))
+display_type(env, Const({"Acc", "rec"}, {v, u}))
 
 -- well_founded_induction_type :
 -- Pi (A : Type)
@@ -34,7 +34,7 @@ local l1          = param_univ("l1")
 local l2          = param_univ("l2")
 local Acc         = Const("Acc", {l1})
 local Acc_intro   = Const("Acc_intro", {l1})
-local Acc_rec     = Const("Acc_rec", {l2, l1})
+local Acc_rec     = Const({"Acc", "rec"}, {l2, l1})
 local A           = Local("A", mk_sort(l1))
 local R           = Local("R", mk_arrow(A, A, Prop))
 local x           = Local("x", A)
@@ -61,5 +61,3 @@ local wfi_th_val  = Fun(A, R, Hwf, P, H, a, Acc_rec(A, R,
 print(env:normalize(type_checker(env):check(wfi_th_val, {l1, l2})))
 env = add_decl(env, mk_definition("well_founded_induction_type", {l1, l2}, wfi_th_type, wfi_th_val))
 display_type(env, Const("well_founded_induction_type", {1,1}))
-
-
diff --git a/tests/lua/alias1.lua b/tests/lua/alias1.lua
index a456e07746..466479745d 100644
--- a/tests/lua/alias1.lua
+++ b/tests/lua/alias1.lua
@@ -30,11 +30,11 @@ env = add_inductive(env,
                     name("list", "cons"), Pi(A, mk_arrow(A, list_l(A), list_l(A))))
 
 env = add_aliases(env, "list", "lst")
-print(not get_expr_aliases(env, {"lst", "list_rec"}):is_nil())
+print(not get_expr_aliases(env, {"lst", "list", "rec"}):is_nil())
 env = add_aliases(env, "list")
-print(get_expr_aliases(env, "list_rec"):head())
-assert(not get_expr_aliases(env, "list_rec"):is_nil())
-assert(not get_expr_aliases(env, {"lst", "list_rec"}):is_nil())
+print(get_expr_aliases(env, {"list", "rec"}):head())
+assert(not get_expr_aliases(env, {"list", "rec"}):is_nil())
+assert(not get_expr_aliases(env, {"lst", "list", "rec"}):is_nil())
 
 env = add_aliases(env, "list", "l")
 print(get_expr_aliases(env, {"l", "list"}):head())
diff --git a/tests/lua/ind1.lua b/tests/lua/ind1.lua
index 05728f3469..e30155cd86 100644
--- a/tests/lua/ind1.lua
+++ b/tests/lua/ind1.lua
@@ -72,9 +72,9 @@ local tc = type_checker(env)
 display_type(env, Const("forest", {0}))
 display_type(env, Const("vcons", {0}))
 display_type(env, Const("consf", {0}))
-display_type(env, Const("forest_rec", {v, u}))
-display_type(env, Const("nat_rec", {v}))
-display_type(env, Const("or_rec"))
+display_type(env, Const({"forest", "rec"}, {v, u}))
+display_type(env, Const({"nat", "rec"}, {v}))
+display_type(env, Const({"or", "rec"}))
 
 local Even = Const("Even")
 local Odd  = Const("Odd")
@@ -100,16 +100,16 @@ local b = Local("b", A)
 env = add_inductive(env,
                     "eq", {l}, 2, Pi(A, a, b, Prop),
                     "refl", Pi(A, a, eq_l(A, a, a)))
-display_type(env, Const("eq_rec", {v, u}))
-display_type(env, Const("exists_rec", {u}))
-display_type(env, Const("list_rec", {v, u}))
-display_type(env, Const("Even_rec"))
-display_type(env, Const("Odd_rec"))
-display_type(env, Const("and_rec", {v}))
-display_type(env, Const("vec_rec", {v, u}))
-display_type(env, Const("flist_rec", {v, u}))
+display_type(env, Const({"eq", "rec"}, {v, u}))
+display_type(env, Const({"exists", "rec"}, {u}))
+display_type(env, Const({"list", "rec"}, {v, u}))
+display_type(env, Const({"Even", "rec"}))
+display_type(env, Const({"Odd", "rec"}))
+display_type(env, Const({"and", "rec"}, {v}))
+display_type(env, Const({"vec", "rec"}, {v, u}))
+display_type(env, Const({"flist", "rec"}, {v, u}))
 
-local nat_rec1 = Const("nat_rec", {1})
+local nat_rec1 = Const({"nat", "rec"}, {1})
 local a        = Local("a", Nat)
 local b        = Local("b", Nat)
 local n        = Local("n", Nat)
@@ -123,7 +123,7 @@ assert(tc:is_def_eq(add(succ(succ(succ(zero))), succ(succ(zero))),
                     succ(succ(succ(succ(succ(zero)))))))
 
 local list_nat      = Const("list", {1})(Nat)
-local list_nat_rec1 = Const("list_rec", {1, 1})(Nat)
+local list_nat_rec1 = Const({"list", "rec"}, {1, 1})(Nat)
 display_type(env, list_nat_rec1)
 local h        = Local("h", Nat)
 local t        = Local("t", list_nat)
@@ -155,4 +155,4 @@ env = env:add_universe("v")
 env = add_inductive(env,
                     "Id", {l}, 1, Pi(A, a, b, U_l),
                     "Id_refl", Pi(A, b, Id_l(A, b, b)))
-display_type(env, Const("Id_rec", {v, u}))
+display_type(env, Const({"Id", "rec"}, {v, u}))
diff --git a/tests/lua/ind3.lua b/tests/lua/ind3.lua
index b0effea388..73770367d0 100644
--- a/tests/lua/ind3.lua
+++ b/tests/lua/ind3.lua
@@ -16,7 +16,7 @@ local a           = Local("a", nat)
 local b           = Local("b", nat)
 local n           = Local("n", nat)
 local r           = Local("r", nat)
-local nat_rec_nat = Const("nat_rec", {1})(Fun(a, nat))
+local nat_rec_nat = Const({"nat", "rec"}, {1})(Fun(a, nat))
 local add         = Fun(a, b, nat_rec_nat(b, Fun(n, r, succ(r)), a))
 local tc          = type_checker(env)
 assert(tc:is_def_eq(add(succ(succ(zero)), succ(zero)),
@@ -48,7 +48,7 @@ local tree_nat        = Const("tree", {1})(nat)
 local tree_list_nat   = Const("tree_list", {1})(nat)
 local t               = Local("t", tree_nat)
 local tl              = Local("tl", tree_list_nat)
-local tree_rec_nat    = Const("tree_rec", {1, 1})(nat, Fun(t, nat), Fun(tl, nat))
+local tree_rec_nat    = Const({"tree", "rec"}, {1, 1})(nat, Fun(t, nat), Fun(tl, nat))
 local r1              = Local("r1", nat)
 local r2              = Local("r2", nat)
 local length_tree_nat = Fun(t, tree_rec_nat(zero,
diff --git a/tests/lua/ind4.lua b/tests/lua/ind4.lua
index 6a37b99697..8cdecb4c32 100644
--- a/tests/lua/ind4.lua
+++ b/tests/lua/ind4.lua
@@ -14,7 +14,7 @@ local env1 = add_inductive(env,
                            "nil", Pi(A, list_l(A)),
                            "cons", Pi(A, mk_arrow(A, list_l(A), list_l(A))))
 
-display_type(env1, Const("list_rec", {1, 1}))
+display_type(env1, Const({"list", "rec"}, {1, 1}))
 
 -- Slightly different definition where A : Type.{l} is an index
 -- instead of a global parameter
@@ -23,8 +23,4 @@ local env2 = add_inductive(env,
                            "list", {l}, 0, Pi(A, U_sl), -- The resultant type must live in the universe succ(l)
                            "nil", Pi(A, list_l(A)),
                            "cons", Pi(A, mk_arrow(A, list_l(A), list_l(A))))
-display_type(env2, Const("list_rec", {1, 1}))
-
-
-
-
+display_type(env2, Const({"list", "rec"}, {1, 1}))
diff --git a/tests/lua/ind5.lua b/tests/lua/ind5.lua
index 210acefa7b..bda6bb2f23 100644
--- a/tests/lua/ind5.lua
+++ b/tests/lua/ind5.lua
@@ -15,7 +15,7 @@ env = env:add_universe("u")
 local a = Local("a", Prop)
 local r = Local("r", retraction)
 
-local rec = Const("retraction_rec")
+local rec = Const({"retraction", "rec"})
 display_type(env, rec)
 local proj = Fun(r, rec(Prop, Fun(a, a), r))
 local inj  = Const("inj")
diff --git a/tests/lua/ind_ex.lua b/tests/lua/ind_ex.lua
index f932c0f9ad..c2a2e8f728 100644
--- a/tests/lua/ind_ex.lua
+++ b/tests/lua/ind_ex.lua
@@ -13,4 +13,4 @@ function display_type(env, t)
    print(tostring(t) .. " : " .. tostring(type_checker(env):check(t)))
 end
 
-display_type(env, Const("inhabited_rec", {1}))
+display_type(env, Const({"inhabited", "rec"}, {1}))
diff --git a/tests/lua/ind_tricky.lua b/tests/lua/ind_tricky.lua
index 1b3b563a5a..ddcdd14169 100644
--- a/tests/lua/ind_tricky.lua
+++ b/tests/lua/ind_tricky.lua
@@ -12,6 +12,6 @@ function display_type(env, t)
 end
 
 env = env:add_universe("u")
-local tricky_rec = Const("tricky_rec", {0})
+local tricky_rec = Const({"tricky", "rec"}, {0})
 
 display_type(env, tricky_rec)
diff --git a/tests/lua/int1.lua b/tests/lua/int1.lua
index e085cf1c82..c43e848263 100644
--- a/tests/lua/int1.lua
+++ b/tests/lua/int1.lua
@@ -15,5 +15,5 @@ function display_type(env, t)
    print(tostring(t) .. " : " .. tostring(type_checker(env):check(t)))
 end
 
-display_type(env, Const("nat_rec", {0}))
-display_type(env, Const("int_rec", {0}))
+display_type(env, Const({"nat", "rec"}, {0}))
+display_type(env, Const({"int", "rec"}, {0}))
diff --git a/tests/lua/sorted.lua b/tests/lua/sorted.lua
index a565dc70d4..38ac74b683 100644
--- a/tests/lua/sorted.lua
+++ b/tests/lua/sorted.lua
@@ -27,5 +27,4 @@ env = add_inductive(env,
                     "is_sorted_cons_nil",  Pi(A, lt, a, is_sorted_l(A, lt, cons_l(A, a, nil_l(A)))),
                     "is_sorted_cons_cons", Pi(A, lt, a1, a2, t, Hlt, Hs, is_sorted_l(A, lt, cons_l(A, a1, cons_l(A, a2, t)))))
 
-print(env:find("is_sorted_rec"):type())
-
+print(env:find({"is_sorted", "rec"}):type())