diff --git a/library/init/classical.lean b/library/init/classical.lean
index 31579e9b61..9e5dc34dce 100644
--- a/library/init/classical.lean
+++ b/library/init/classical.lean
@@ -5,7 +5,6 @@ Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 -/
 prelude
 import init.data.subtype.basic init.funext
-open subtype
 
 namespace classical
 universes u v
@@ -18,10 +17,10 @@ noncomputable theorem indefinite_description {α : Sort u} (p : α → Prop) :
 λ h, choice (let ⟨x, px⟩ := h in ⟨⟨x, px⟩⟩)
 
 noncomputable def some {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : α :=
-elt_of (indefinite_description p h)
+(indefinite_description p h)^.val
 
 theorem some_spec {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : p (some h) :=
-has_property (indefinite_description p h)
+(indefinite_description p h)^.property
 
 /- Diaconescu's theorem: using function extensionality and propositional extensionality,
    we can get excluded middle from this. -/
@@ -76,7 +75,7 @@ theorem exists_true_of_nonempty {α : Sort u} (h : nonempty α) : ∃ x : α, tr
 nonempty.elim h (take x, ⟨x, trivial⟩)
 
 noncomputable def inhabited_of_nonempty {α : Sort u} (h : nonempty α) : inhabited α :=
-⟨elt_of (indefinite_description _ (exists_true_of_nonempty h))⟩
+⟨(indefinite_description _ (exists_true_of_nonempty h))^.val⟩
 
 noncomputable def inhabited_of_exists {α : Sort u} {p : α → Prop} (h : ∃ x, p x) :
   inhabited α :=
@@ -107,18 +106,19 @@ noncomputable theorem strong_indefinite_description {α : Sort u} (p : α → Pr
   (h : nonempty α) : { x : α // (∃ y : α, p y) → p x} :=
 match (prop_decidable (∃ x : α, p x)) with
 | (is_true hp)  := let xp := indefinite_description _ hp in
-                   tag (elt_of xp) (λ h', has_property xp)
-| (is_false hn) := tag (@inhabited.default _ (inhabited_of_nonempty h)) (λ h, absurd h hn)
+                   ⟨xp^.val, λ h', xp^.property⟩
+| (is_false hn) := ⟨@inhabited.default _ (inhabited_of_nonempty h), λ h, absurd h hn⟩
 end
 
 /- the Hilbert epsilon function -/
 
 noncomputable def epsilon {α : Sort u} [h : nonempty α] (p : α → Prop) : α :=
-elt_of (strong_indefinite_description p h)
+(strong_indefinite_description p h)^.val
 
 theorem epsilon_spec_aux {α : Sort u} (h : nonempty α) (p : α → Prop) (hex : ∃ y, p y) :
     p (@epsilon α h p) :=
-have aux : (∃ y, p y) → p (elt_of (strong_indefinite_description p h)), from has_property (strong_indefinite_description p h),
+have aux : (∃ y, p y) → p ((strong_indefinite_description p h)^.val),
+  from (strong_indefinite_description p h)^.property,
 aux hex
 
 theorem epsilon_spec {α : Sort u} {p : α → Prop} (hex : ∃ y, p y) :
diff --git a/library/init/coe.lean b/library/init/coe.lean
index 4d34dcb75a..f9a9e13264 100644
--- a/library/init/coe.lean
+++ b/library/init/coe.lean
@@ -150,7 +150,7 @@ instance coe_decidable_eq (x : bool) : decidable (coe x) :=
 show decidable (x = tt), from bool.decidable_eq x tt
 
 instance coe_subtype {a : Type u} {p : a → Prop} : has_coe {x // p x} a :=
-⟨λ s, subtype.elt_of s⟩
+⟨subtype.val⟩
 
 /- basic lifts -/
 
diff --git a/library/init/core.lean b/library/init/core.lean
index 4e03b87a51..36ec5e08f8 100644
--- a/library/init/core.lean
+++ b/library/init/core.lean
@@ -196,7 +196,7 @@ inductive bool : Type
 
 /- Remark: subtype must take a Sort instead of Type because of the axiom strong_indefinite_description. -/
 structure subtype {α : Sort u} (p : α → Prop) :=
-tag :: (elt_of : α) (has_property : p elt_of)
+(val : α) (property : p val)
 
 class inductive decidable (p : Prop)
 | is_false : ¬p → decidable
diff --git a/library/init/data/subtype/basic.lean b/library/init/data/subtype/basic.lean
index 8fdf0e255d..be0a766c35 100644
--- a/library/init/data/subtype/basic.lean
+++ b/library/init/data/subtype/basic.lean
@@ -16,10 +16,10 @@ def exists_of_subtype {α : Type u} {p : α → Prop} : { x // p x } → ∃ x,
 
 variables {α : Type u} {p : α → Prop}
 
-lemma tag_irrelevant {a : α} (h1 h2 : p a) : tag a h1 = tag a h2 :=
+lemma tag_irrelevant {a : α} (h1 h2 : p a) : mk a h1 = mk a h2 :=
 rfl
 
-protected lemma eq : ∀ {a1 a2 : {x // p x}}, elt_of a1 = elt_of a2 → a1 = a2
+protected lemma eq : ∀ {a1 a2 : {x // p x}}, val a1 = val a2 → a1 = a2
 | ⟨x, h1⟩ ⟨.x, h2⟩ rfl := rfl
 
 end subtype
diff --git a/library/init/data/to_string.lean b/library/init/data/to_string.lean
index 4bcd586919..49df129bab 100644
--- a/library/init/data/to_string.lean
+++ b/library/init/data/to_string.lean
@@ -51,7 +51,7 @@ instance {α : Type u} {β : α → Type v} [has_to_string α] [s : ∀ x, has_t
 ⟨λ ⟨a, b⟩, "⟨"  ++ to_string a ++ ", " ++ to_string b ++ "⟩"⟩
 
 instance {α : Type u} {p : α → Prop} [has_to_string α] : has_to_string (subtype p) :=
-⟨λ s, to_string (elt_of s)⟩
+⟨λ s, to_string (val s)⟩
 
 /- Remark: the code generator replaces this definition with one that display natural numbers in decimal notation -/
 protected def nat.to_string : nat → string
diff --git a/library/init/meta/format.lean b/library/init/meta/format.lean
index 4bfff9d839..edcfaea44b 100644
--- a/library/init/meta/format.lean
+++ b/library/init/meta/format.lean
@@ -120,7 +120,7 @@ meta instance {α : Type u} {β : α → Type v} [has_to_format α] [s : ∀ x,
 open subtype
 
 meta instance {α : Type u} {p : α → Prop} [has_to_format α] : has_to_format (subtype p) :=
-⟨λ s, to_fmt (elt_of s)⟩
+⟨λ s, to_fmt (val s)⟩
 
 meta def format.bracket : string → string → format → format
 | o c f := to_fmt o ++ nest (utf8_length o) f ++ to_fmt c