diff --git a/library/algebra/category.lean b/library/algebra/category.lean
index 52afce45e..a44e2a328 100644
--- a/library/algebra/category.lean
+++ b/library/algebra/category.lean
@@ -61,11 +61,11 @@ namespace category
     i = id ∘ i : eq.symm id_left
     ... = id : H
 
-  inductive is_section {A B : ob} (f : mor A B) : Type :=
+  inductive is_section [class] {A B : ob} (f : mor A B) : Type :=
   mk : ∀{g}, g ∘ f = id → is_section f
-  inductive is_retraction {A B : ob} (f : mor A B) : Type :=
+  inductive is_retraction [class] {A B : ob} (f : mor A B) : Type :=
   mk : ∀{g}, f ∘ g = id → is_retraction f
-  inductive is_iso {A B : ob} (f : mor A B) : Type :=
+  inductive is_iso [class] {A B : ob} (f : mor A B) : Type :=
   mk : ∀{g}, g ∘ f = id → f ∘ g = id → is_iso f
 
   definition retraction_of {A B : ob} (f : mor A B) {H : is_section f} : mor B A :=
diff --git a/library/algebra/relation.lean b/library/algebra/relation.lean
index 065fe5a6c..015f9b38d 100644
--- a/library/algebra/relation.lean
+++ b/library/algebra/relation.lean
@@ -18,7 +18,7 @@ definition symmetric {T : Type} (R : T → T → Type) : Type := ∀⦃x y⦄, R
 definition transitive {T : Type} (R : T → T → Type) : Type := ∀⦃x y z⦄, R x y → R y z → R x z
 
 
-inductive is_reflexive {T : Type} (R : T → T → Type) : Prop :=
+inductive is_reflexive [class] {T : Type} (R : T → T → Type) : Prop :=
 mk : reflexive R → is_reflexive R
 
 namespace is_reflexive
@@ -32,7 +32,7 @@ namespace is_reflexive
 end is_reflexive
 
 
-inductive is_symmetric {T : Type} (R : T → T → Type) : Prop :=
+inductive is_symmetric [class] {T : Type} (R : T → T → Type) : Prop :=
 mk : symmetric R → is_symmetric R
 
 namespace is_symmetric
@@ -46,7 +46,7 @@ namespace is_symmetric
 end is_symmetric
 
 
-inductive is_transitive {T : Type} (R : T → T → Type) : Prop :=
+inductive is_transitive [class] {T : Type} (R : T → T → Type) : Prop :=
 mk : transitive R → is_transitive R
 
 namespace is_transitive
@@ -60,7 +60,7 @@ namespace is_transitive
 end is_transitive
 
 
-inductive is_equivalence {T : Type} (R : T → T → Type) : Prop :=
+inductive is_equivalence [class] {T : Type} (R : T → T → Type) : Prop :=
 mk : is_reflexive R → is_symmetric R → is_transitive R → is_equivalence R
 
 theorem is_equivalence.is_reflexive [instance]
@@ -90,12 +90,12 @@ theorem is_PER.is_transitive [instance]
 -- Congruence for unary and binary functions
 -- -----------------------------------------
 
-inductive congruence {T1 : Type} (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop)
+inductive congruence [class] {T1 : Type} (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop)
     (f : T1 → T2) : Prop :=
 mk : (∀x y, R1 x y → R2 (f x) (f y)) → congruence R1 R2 f
 
 -- for binary functions
-inductive congruence2 {T1 : Type}  (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop)
+inductive congruence2 [class] {T1 : Type}  (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop)
     {T3 : Type} (R3 : T3 → T3 → Prop) (f : T1 → T2 → T3) : Prop :=
 mk : (∀(x1 y1 : T1) (x2 y2 : T2), R1 x1 y1 → R2 x2 y2 → R3 (f x1 x2) (f y1 y2)) →
     congruence2 R1 R2 R3 f
@@ -161,7 +161,7 @@ congruence.mk (λx y H, H)
 -- Relations that can be coerced to functions / implications
 -- ---------------------------------------------------------
 
-inductive mp_like {R : Type → Type → Prop} {a b : Type} (H : R a b) : Type :=
+inductive mp_like [class] {R : Type → Type → Prop} {a b : Type} (H : R a b) : Type :=
 mk {} : (a → b) → @mp_like R a b H
 
 namespace mp_like
diff --git a/library/hott/fibrant.lean b/library/hott/fibrant.lean
index 6bf736316..7760a7584 100644
--- a/library/hott/fibrant.lean
+++ b/library/hott/fibrant.lean
@@ -7,7 +7,7 @@ import data.prod data.sum data.sigma
 
 open unit bool nat prod sum sigma
 
-inductive fibrant (T : Type) : Type :=
+inductive fibrant [class] (T : Type) : Type :=
 fibrant_mk : fibrant T
 
 namespace fibrant
diff --git a/library/logic/decidable.lean b/library/logic/decidable.lean
index cf76b746d..76cf4eb4b 100644
--- a/library/logic/decidable.lean
+++ b/library/logic/decidable.lean
@@ -4,7 +4,7 @@
 
 import logic.connectives
 
-inductive decidable (p : Prop) : Type :=
+inductive decidable [class] (p : Prop) : Type :=
 inl : p  → decidable p,
 inr : ¬p → decidable p
 
diff --git a/library/logic/inhabited.lean b/library/logic/inhabited.lean
index 23e672800..7b3b771d1 100644
--- a/library/logic/inhabited.lean
+++ b/library/logic/inhabited.lean
@@ -4,7 +4,7 @@
 
 import logic.connectives
 
-inductive inhabited (A : Type) : Type :=
+inductive inhabited [class] (A : Type) : Type :=
 mk : A → inhabited A
 
 namespace inhabited
diff --git a/library/logic/nonempty.lean b/library/logic/nonempty.lean
index f787b7c16..c620c76da 100644
--- a/library/logic/nonempty.lean
+++ b/library/logic/nonempty.lean
@@ -4,7 +4,7 @@
 import .inhabited
 open inhabited
 
-inductive nonempty (A : Type) : Prop :=
+inductive nonempty [class] (A : Type) : Prop :=
 intro : A → nonempty A
 
 namespace nonempty
diff --git a/src/frontends/lean/class.cpp b/src/frontends/lean/class.cpp
index ccca79f5f..733e926be 100644
--- a/src/frontends/lean/class.cpp
+++ b/src/frontends/lean/class.cpp
@@ -123,11 +123,17 @@ static void check_class(environment const & env, name const & c_name) {
         throw exception(sstream() << "invalid class, '" << c_name << "' is a definition");
 }
 
+static void check_is_class(environment const & env, name const & c_name) {
+    class_state const & s = class_ext::get_state(env);
+    if (!s.m_instances.contains(c_name))
+        throw exception(sstream() << "'" << c_name << "' is not a class");
+}
+
 name get_class_name(environment const & env, expr const & e) {
     if (!is_constant(e))
         throw exception("class expected, expression is not a constant");
     name const & c_name = const_name(e);
-    check_class(env, c_name);
+    check_is_class(env, c_name);
     return c_name;
 }
 
@@ -156,7 +162,7 @@ environment add_instance(environment const & env, name const & n, unsigned prior
         type = instantiate(binding_body(type), mk_local(ngen.next(), binding_domain(type)));
     }
     name c = get_class_name(env, get_app_fn(type));
-    check_class(env, c);
+    check_is_class(env, c);
     return class_ext::add_entry(env, get_dummy_ios(), class_entry(c, n, priority), persistent);
 }
 
diff --git a/tests/lean/bad_class.lean b/tests/lean/bad_class.lean
new file mode 100644
index 000000000..df38cfa1d
--- /dev/null
+++ b/tests/lean/bad_class.lean
@@ -0,0 +1,7 @@
+import logic
+
+definition subsingleton (A : Type) := ∀⦃a b : A⦄, a = b
+class subsingleton
+
+protected definition prop.subsingleton [instance] (P : Prop) : subsingleton P :=
+λa b, !proof_irrel
diff --git a/tests/lean/bad_class.lean.expected.out b/tests/lean/bad_class.lean.expected.out
new file mode 100644
index 000000000..4fe2501b9
--- /dev/null
+++ b/tests/lean/bad_class.lean.expected.out
@@ -0,0 +1,2 @@
+bad_class.lean:4:0: error: invalid class, 'subsingleton' is a definition
+bad_class.lean:6:0: error: 'eq' is not a class
diff --git a/tests/lean/inst.lean b/tests/lean/inst.lean
index 5a44e453b..6a87d2a70 100644
--- a/tests/lean/inst.lean
+++ b/tests/lean/inst.lean
@@ -2,7 +2,7 @@ import logic data.prod priority
 open priority
 set_option pp.notation false
 
-inductive C (A : Type) :=
+inductive C [class] (A : Type) :=
 mk : A → C A
 
 definition val {A : Type} (c : C A) : A :=
diff --git a/tests/lean/run/algebra1.lean b/tests/lean/run/algebra1.lean
index 32f5c3b46..15b983bed 100644
--- a/tests/lean/run/algebra1.lean
+++ b/tests/lean/run/algebra1.lean
@@ -15,10 +15,10 @@ context
 end
 
 namespace algebra
-  inductive mul_struct (A : Type) : Type :=
+  inductive mul_struct [class] (A : Type) : Type :=
   mk : (A → A → A) → mul_struct A
 
-  inductive add_struct (A : Type) : Type :=
+  inductive add_struct [class] (A : Type) : Type :=
   mk : (A → A → A) → add_struct A
 
   definition mul  {A : Type} {s : mul_struct A} (a b : A)
@@ -32,6 +32,7 @@ namespace algebra
   infixl `+`:65 := add
 end algebra
 
+open algebra
   inductive nat : Type :=
   zero : nat,
   succ : nat → nat
@@ -54,7 +55,7 @@ end nat
 
 namespace algebra
 namespace semigroup
-  inductive semigroup_struct (A : Type) : Type :=
+  inductive semigroup_struct [class] (A : Type) : Type :=
   mk : Π (mul : A → A → A), is_assoc mul → semigroup_struct A
 
   definition mul  {A : Type} (s : semigroup_struct A) (a b : A)
@@ -79,7 +80,7 @@ end semigroup
 namespace monoid
   check semigroup.mul
 
-  inductive monoid_struct (A : Type) : Type :=
+  inductive monoid_struct [class] (A : Type) : Type :=
   mk_monoid_struct : Π (mul : A → A → A) (id : A), is_assoc mul → is_id mul id → monoid_struct A
 
   definition mul  {A : Type} (s : monoid_struct A) (a b : A)
diff --git a/tests/lean/run/class4.lean b/tests/lean/run/class4.lean
index cf0aac9bf..4d1f3f544 100644
--- a/tests/lean/run/class4.lean
+++ b/tests/lean/run/class4.lean
@@ -56,7 +56,7 @@ theorem not_zero_add (x y : nat) (H : ¬ is_zero y) : ¬ is_zero (x + y)
           not_is_zero_succ (x+w),
         subst (symm H1) H2)
 
-inductive not_zero (x : nat) : Prop :=
+inductive not_zero [class] (x : nat) : Prop :=
 intro : ¬ is_zero x → not_zero x
 
 theorem not_zero_not_is_zero {x : nat} (H : not_zero x) : ¬ is_zero x
diff --git a/tests/lean/run/class5.lean b/tests/lean/run/class5.lean
index 6615364c6..2b2504985 100644
--- a/tests/lean/run/class5.lean
+++ b/tests/lean/run/class5.lean
@@ -1,7 +1,7 @@
 import logic
 
 namespace algebra
-  inductive mul_struct (A : Type) : Type :=
+  inductive mul_struct [class] (A : Type) : Type :=
   mk : (A → A → A) → mul_struct A
 
   definition mul {A : Type} {s : mul_struct A} (a b : A)
@@ -10,6 +10,7 @@ namespace algebra
   infixl `*`:75 := mul
 end algebra
 
+open algebra
 namespace nat
   inductive nat : Type :=
   zero : nat,
diff --git a/tests/lean/run/class7.lean b/tests/lean/run/class7.lean
index 7c525defc..320450d2e 100644
--- a/tests/lean/run/class7.lean
+++ b/tests/lean/run/class7.lean
@@ -1,7 +1,7 @@
 import logic
 open tactic
 
-inductive inh (A : Type) : Type :=
+inductive inh [class] (A : Type) : Type :=
 intro : A -> inh A
 
 theorem inh_bool [instance] : inh Prop
diff --git a/tests/lean/run/class8.lean b/tests/lean/run/class8.lean
index 4ace94760..aa7db0f1c 100644
--- a/tests/lean/run/class8.lean
+++ b/tests/lean/run/class8.lean
@@ -1,7 +1,7 @@
 import logic data.prod
 open tactic prod
 
-inductive inh (A : Type) : Prop :=
+inductive inh [class] (A : Type) : Prop :=
 intro : A -> inh A
 
 instance inh.intro
diff --git a/tests/lean/run/class_coe.lean b/tests/lean/run/class_coe.lean
index b4b28638d..b6d84c8d4 100644
--- a/tests/lean/run/class_coe.lean
+++ b/tests/lean/run/class_coe.lean
@@ -6,7 +6,7 @@ constant nat_add  : nat → nat → nat
 constant int_add  : int → int → int
 constant real_add : real → real → real
 
-inductive add_struct (A : Type) :=
+inductive add_struct [class] (A : Type) :=
 mk : (A → A → A) → add_struct A
 
 definition add {A : Type} {S : add_struct A} (a b : A) : A :=
diff --git a/tests/lean/run/congr_imp_bug.lean b/tests/lean/run/congr_imp_bug.lean
index a0955cd2e..ce4037d45 100644
--- a/tests/lean/run/congr_imp_bug.lean
+++ b/tests/lean/run/congr_imp_bug.lean
@@ -8,7 +8,7 @@ open function
 
 namespace congr
 
-inductive struc {T1 : Type} {T2 : Type} (R1 : T1 → T1 → Prop) (R2 : T2 → T2 → Prop)
+inductive struc [class] {T1 : Type} {T2 : Type} (R1 : T1 → T1 → Prop) (R2 : T2 → T2 → Prop)
     (f : T1 → T2) : Prop :=
 mk : (∀x y : T1, R1 x y → R2 (f x) (f y)) → struc R1 R2 f
 
diff --git a/tests/lean/run/elab_bug1.lean b/tests/lean/run/elab_bug1.lean
index b571e9b10..d0e5a768e 100644
--- a/tests/lean/run/elab_bug1.lean
+++ b/tests/lean/run/elab_bug1.lean
@@ -16,7 +16,7 @@ definition reflexive {T : Type} (R : T → T → Prop) : Prop := ∀x, R x x
 -- Congruence classes for unary and binary functions
 -- -------------------------------------------------
 
-inductive congruence {T1 : Type} {T2 : Type} (R1 : T1 → T1 → Prop) (R2 : T2 → T2 → Prop)
+inductive congruence [class] {T1 : Type} {T2 : Type} (R1 : T1 → T1 → Prop) (R2 : T2 → T2 → Prop)
     (f : T1 → T2) : Prop :=
 mk : (∀x y : T1, R1 x y → R2 (f x) (f y)) → congruence R1 R2 f
 
diff --git a/tests/lean/run/group.lean b/tests/lean/run/group.lean
index ac1dcac07..bb5635948 100644
--- a/tests/lean/run/group.lean
+++ b/tests/lean/run/group.lean
@@ -12,7 +12,7 @@ context
   definition is_inv   := ∀ a, a*a^-1 = one
 end
 
-inductive group_struct (A : Type) : Type :=
+inductive group_struct [class] (A : Type) : Type :=
 mk_group_struct : Π (mul : A → A → A) (one : A) (inv : A → A), is_assoc mul → is_id mul one → is_inv mul one inv → group_struct A
 
 inductive group : Type :=
diff --git a/tests/lean/run/group2.lean b/tests/lean/run/group2.lean
index ed5b941f4..fcc9263b3 100644
--- a/tests/lean/run/group2.lean
+++ b/tests/lean/run/group2.lean
@@ -12,7 +12,7 @@ context
   definition is_inv   := ∀ a, a*a^-1 = one
 end
 
-inductive group_struct (A : Type) : Type :=
+inductive group_struct [class] (A : Type) : Type :=
 mk : Π (mul : A → A → A) (one : A) (inv : A → A), is_assoc mul → is_id mul one → is_inv mul one inv → group_struct A
 
 inductive group : Type :=
diff --git a/tests/lean/run/group3.lean b/tests/lean/run/group3.lean
index 3921a8eba..9a5d16ae0 100644
--- a/tests/lean/run/group3.lean
+++ b/tests/lean/run/group3.lean
@@ -56,7 +56,7 @@ section
   include s
   definition semigroup_has_mul [instance] : has_mul A := has_mul.mk semigroup.mul
 
-  theorem mul_assoc [instance] (a b c : A) : a * b * c = a * (b * c) :=
+  theorem mul_assoc (a b c : A) : a * b * c = a * (b * c) :=
     !semigroup.assoc
 end
 
diff --git a/tests/lean/run/univ_bug1.lean b/tests/lean/run/univ_bug1.lean
index 6ba5fd71d..61e13da32 100644
--- a/tests/lean/run/univ_bug1.lean
+++ b/tests/lean/run/univ_bug1.lean
@@ -12,7 +12,7 @@ namespace simp
 -- set_option pp.implicit true
 
 -- first define a class of homogeneous equality
-inductive simplifies_to {T : Type} (t1 t2 : T) : Prop :=
+inductive simplifies_to [class] {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 :=
diff --git a/tests/lean/run/univ_bug2.lean b/tests/lean/run/univ_bug2.lean
index 219f85180..cb12a4a14 100644
--- a/tests/lean/run/univ_bug2.lean
+++ b/tests/lean/run/univ_bug2.lean
@@ -8,7 +8,7 @@ import logic data.nat
 open nat
 
 -- first define a class of homogeneous equality
-inductive simplifies_to {T : Type} (t1 t2 : T) : Prop :=
+inductive simplifies_to [class] {T : Type} (t1 t2 : T) : Prop :=
 mk : t1 = t2 → simplifies_to t1 t2
 
 namespace simplifies_to
diff --git a/tests/lean/slow/cat_sec_var_bug.lean b/tests/lean/slow/cat_sec_var_bug.lean
index 599d4828f..01c597adb 100644
--- a/tests/lean/slow/cat_sec_var_bug.lean
+++ b/tests/lean/slow/cat_sec_var_bug.lean
@@ -60,9 +60,9 @@ namespace category
     i = id ∘ i : eq.symm !id_left
     ... = id : H
 
-  inductive is_section    (f : hom a b) : Type := mk : ∀{g}, g ∘ f = id → is_section f
-  inductive is_retraction (f : hom a b) : Type := mk : ∀{g}, f ∘ g = id → is_retraction f
-  inductive is_iso        (f : hom a b) : Type := mk : ∀{g}, g ∘ f = id → f ∘ g = id → is_iso f
+  inductive is_section    [class] (f : hom a b) : Type := mk : ∀{g}, g ∘ f = id → is_section f
+  inductive is_retraction [class] (f : hom a b) : Type := mk : ∀{g}, f ∘ g = id → is_retraction f
+  inductive is_iso        [class] (f : hom a b) : Type := mk : ∀{g}, g ∘ f = id → f ∘ g = id → is_iso f
 
   definition retraction_of (f : hom a b) {H : is_section f} : hom b a :=
   is_section.rec (λg h, g) H