diff --git a/library/standard/decidable.lean b/library/standard/decidable.lean
index 5a49b0702..37c0b5d7a 100644
--- a/library/standard/decidable.lean
+++ b/library/standard/decidable.lean
@@ -14,7 +14,7 @@ theorem induction_on {p : Prop} {C : Prop} (H : decidable p) (H1 : p → C) (H2
 theorem em (p : Prop) (H : decidable p) : p ∨ ¬p
 := induction_on H (λ Hp, or_intro_left _ Hp) (λ Hnp, or_intro_right _ Hnp)
 
-definition rec [inline] {p : Prop} {C : Type} (H : decidable p) (H1 : p → C) (H2 : ¬p → C) : C
+definition rec_on [inline] {p : Prop} {C : Type} (H : decidable p) (H1 : p → C) (H2 : ¬p → C) : C
 := decidable_rec H1 H2 H
 
 theorem irrelevant {p : Prop} (d1 d2 : decidable p) : d1 = d2
@@ -36,36 +36,36 @@ theorem decidable_false [instance] : decidable false
 := inr not_false_trivial
 
 theorem decidable_and [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) : decidable (a ∧ b)
-:= rec Ha
-    (assume Ha  : a, rec Hb
+:= rec_on Ha
+    (assume Ha  : a, rec_on Hb
       (assume Hb  : b,  inl (and_intro Ha Hb))
       (assume Hnb : ¬b, inr (and_not_right a Hnb)))
     (assume Hna : ¬a, inr (and_not_left b Hna))
 
 theorem decidable_or [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) : decidable (a ∨ b)
-:= rec Ha
+:= rec_on Ha
     (assume Ha  : a, inl (or_intro_left b Ha))
-    (assume Hna : ¬a, rec Hb
+    (assume Hna : ¬a, rec_on Hb
       (assume Hb  : b,  inl (or_intro_right a Hb))
       (assume Hnb : ¬b, inr (or_not_intro Hna Hnb)))
 
 theorem decidable_not [instance] {a : Prop} (Ha : decidable a) : decidable (¬a)
-:= rec Ha
+:= rec_on Ha
     (assume Ha,  inr (not_not_intro Ha))
     (assume Hna, inl Hna)
 
 theorem decidable_iff [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) : decidable (a ↔ b)
-:= rec Ha
-    (assume Ha, rec Hb
+:= rec_on Ha
+    (assume Ha, rec_on Hb
       (assume Hb  : b,  inl (iff_intro (assume H, Hb) (assume H, Ha)))
       (assume Hnb : ¬b, inr (not_intro (assume H : a ↔ b, absurd (iff_mp_left H Ha) Hnb))))
-    (assume Hna, rec Hb
+    (assume Hna, rec_on Hb
       (assume Hb  : b,  inr (not_intro (assume H : a ↔ b, absurd (iff_mp_right H Hb) Hna)))
       (assume Hnb : ¬b, inl (iff_intro (assume Ha, absurd_elim b Ha Hna) (assume Hb, absurd_elim a Hb Hnb))))
 
 theorem decidable_implies [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) : decidable (a → b)
-:= rec Ha
-    (assume Ha  : a, rec Hb
+:= rec_on Ha
+    (assume Ha  : a, rec_on Hb
       (assume Hb  : b,  inl (assume H, Hb))
       (assume Hnb : ¬b, inr (not_intro (assume H : a → b,
         absurd (H Ha) Hnb))))
diff --git a/library/standard/if.lean b/library/standard/if.lean
index a93592189..bb3f16329 100644
--- a/library/standard/if.lean
+++ b/library/standard/if.lean
@@ -5,7 +5,7 @@ import decidable tactic
 using decidable tactic
 
 definition ite (c : Prop) {H : decidable c} {A : Type} (t e : A) : A
-:= rec H (assume Hc,  t) (assume Hnc, e)
+:= rec_on H (assume Hc,  t) (assume Hnc, e)
 
 notation `if` c `then` t `else` e:45 := ite c t e