diff --git a/library/Init/Lean/Class.lean b/library/Init/Lean/Class.lean
index 755ff41682..8841815e69 100644
--- a/library/Init/Lean/Class.lean
+++ b/library/Init/Lean/Class.lean
@@ -91,7 +91,8 @@ def addClass (env : Environment) (clsName : Name) : Except String Environment :=
 if isClass env clsName then Except.error ("class has already been declared '" ++ toString clsName ++ "'")
 else match env.find clsName with
   | none      => Except.error ("unknown declaration '" ++ toString clsName ++ "'")
-  | some decl => Except.ok (classExtension.addEntry env (ClassEntry.«class» clsName decl.type.hasOutParam))
+  | some decl@(ConstantInfo.inductInfo _) => Except.ok (classExtension.addEntry env (ClassEntry.«class» clsName decl.type.hasOutParam))
+  | some _    => Except.error ("invalid 'class', declaration '" ++ toString clsName ++ "' must be inductive datatype or structure")
 
 private def consumeNLambdas : Nat → Expr → Option Expr
 | 0,   e                => some e
diff --git a/tests/lean/class_def_must_fail.lean b/tests/lean/class_def_must_fail.lean
new file mode 100644
index 0000000000..7ec170cd62
--- /dev/null
+++ b/tests/lean/class_def_must_fail.lean
@@ -0,0 +1,7 @@
+/- The following definition should fail. -/
+@[class] def Foo (n : Nat) : Prop := n > 2
+
+
+def Bla (n : Nat) : Prop := n > 2
+
+attribute [class] Bla
diff --git a/tests/lean/class_def_must_fail.lean.expected.out b/tests/lean/class_def_must_fail.lean.expected.out
new file mode 100644
index 0000000000..9f9cfcb007
--- /dev/null
+++ b/tests/lean/class_def_must_fail.lean.expected.out
@@ -0,0 +1,2 @@
+class_def_must_fail.lean:2:13: error: invalid 'class', declaration 'Foo' must be inductive datatype or structure
+class_def_must_fail.lean:7:0: error: invalid 'class', declaration 'Bla' must be inductive datatype or structure
diff --git a/tests/lean/fail/typeclass_outparam.lean b/tests/lean/fail/typeclass_outparam.lean
index 23066bc4a0..7282657202 100644
--- a/tests/lean/fail/typeclass_outparam.lean
+++ b/tests/lean/fail/typeclass_outparam.lean
@@ -1,5 +1,4 @@
-@[class] axiom OPClass (α : outParam Type) (β : Type) : Type
-
-@[instance] axiom op₁ : OPClass Nat Nat
+class OPClass (α : outParam Type) (β : Type) : Type := (u : Unit := ())
+instance op₁ : OPClass Nat Nat := {}
 
 #synth OPClass Bool Nat
diff --git a/tests/lean/run/typeclass_append.lean b/tests/lean/run/typeclass_append.lean
index 56daf80bee..f4c526198c 100644
--- a/tests/lean/run/typeclass_append.lean
+++ b/tests/lean/run/typeclass_append.lean
@@ -6,9 +6,14 @@ Authors: Daniel Selsam
 Performance test to ensure quadratic blowup is avoided.
 -/
 
-@[class] axiom Append {α : Type} (xs₁ xs₂ : List α) (out : outParam $ List α) : Type
-@[instance] axiom AppendBase {α : Type} (xs₂ : List α) : Append [] xs₂ xs₂
-@[instance] axiom AppendStep {α : Type} (x : α) (xs₁ xs₂ out : List α) [Append xs₁ xs₂ out] : Append (x::xs₁) xs₂ (x::out)
+class Append {α : Type} (xs₁ xs₂ : List α) (out : outParam $ List α) : Type :=
+(u : Unit := ())
+
+instance AppendBase {α : Type} (xs₂ : List α) : Append [] xs₂ xs₂ :=
+{}
+
+instance AppendStep {α : Type} (x : α) (xs₁ xs₂ out : List α) [Append xs₁ xs₂ out] : Append (x::xs₁) xs₂ (x::out) :=
+{}
 
 #synth Append
 [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90, 91, 92, 93, 94, 95, 96, 97, 98, 99, 100, 101, 102, 103, 104, 105, 106, 107, 108, 109, 110, 111, 112, 113, 114, 115, 116, 117, 118, 119, 120, 121, 122, 123, 124, 125, 126, 127, 128, 129, 130, 131, 132, 133, 134, 135, 136, 137, 138, 139, 140, 141, 142, 143, 144, 145, 146, 147, 148, 149, 150, 151, 152, 153, 154, 155, 156, 157, 158, 159, 160, 161, 162, 163, 164, 165, 166, 167, 168, 169, 170, 171, 172, 173, 174, 175, 176, 177, 178, 179, 180, 181, 182, 183, 184, 185, 186, 187, 188, 189, 190, 191, 192, 193, 194, 195, 196, 197, 198, 199]
diff --git a/tests/lean/run/typeclass_diamond.lean b/tests/lean/run/typeclass_diamond.lean
index 7624602bde..c42238917d 100644
--- a/tests/lean/run/typeclass_diamond.lean
+++ b/tests/lean/run/typeclass_diamond.lean
@@ -1,30 +1,30 @@
-@[class] axiom Top₁   (n : Nat) : Type
-@[class] axiom Bot₁   (n : Nat) : Type
-@[class] axiom Left₁  (n : Nat) : Type
-@[class] axiom Right₁ (n : Nat) : Type
+class Top₁   (n : Nat) : Type := (u : Unit := ())
+class Bot₁   (n : Nat) : Type := (u : Unit := ())
+class Left₁  (n : Nat) : Type := (u : Unit := ())
+class Right₁ (n : Nat) : Type := (u : Unit := ())
 
-@[instance] axiom Bot₁Inst : Bot₁ Nat.zero
+instance Bot₁Inst : Bot₁ Nat.zero := {}
+instance Left₁ToBot₁   (n : Nat) [Left₁ n]  : Bot₁ n := {}
 
-@[instance] axiom Left₁ToBot₁   (n : Nat) [Left₁ n]  : Bot₁ n
-@[instance] axiom Right₁ToBot₁  (n : Nat) [Right₁ n] : Bot₁ n
-@[instance] axiom Top₁ToLeft₁   (n : Nat) [Top₁ n]   : Left₁ n
-@[instance] axiom Top₁ToRight₁  (n : Nat) [Top₁ n]   : Right₁ n
-@[instance] axiom Bot₁ToTopSucc (n : Nat) [Bot₁ n]   : Top₁ n.succ
+instance Right₁ToBot₁  (n : Nat) [Right₁ n] : Bot₁ n := {}
+instance Top₁ToLeft₁   (n : Nat) [Top₁ n]   : Left₁ n := {}
+instance Top₁ToRight₁  (n : Nat) [Top₁ n]   : Right₁ n := {}
+instance Bot₁ToTopSucc (n : Nat) [Bot₁ n]   : Top₁ n.succ := {}
 
-@[class] axiom Top₂ (n : Nat) : Type
-@[class] axiom Bot₂   (n : Nat) : Type
-@[class] axiom Left₂  (n : Nat) : Type
-@[class] axiom Right₂ (n : Nat) : Type
+class Top₂ (n : Nat) : Type := (u : Unit := ())
+class Bot₂   (n : Nat) : Type := (u : Unit := ())
+class Left₂  (n : Nat) : Type := (u : Unit := ())
+class Right₂ (n : Nat) : Type := (u : Unit := ())
 
-@[instance] axiom Left₂ToBot₂   (n : Nat) [Left₂ n]  : Bot₂ n
-@[instance] axiom Right₂ToBot₂  (n : Nat) [Right₂ n] : Bot₂ n
-@[instance] axiom Top₂ToLeft₂   (n : Nat) [Top₂ n]   : Left₂ n
-@[instance] axiom Top₂ToRight₂  (n : Nat) [Top₂ n]   : Right₂ n
-@[instance] axiom Bot₂ToTopSucc (n : Nat) [Bot₂ n]   : Top₂ n.succ
+instance Left₂ToBot₂   (n : Nat) [Left₂ n]  : Bot₂ n := {}
+instance Right₂ToBot₂  (n : Nat) [Right₂ n] : Bot₂ n := {}
+instance Top₂ToLeft₂   (n : Nat) [Top₂ n]   : Left₂ n := {}
+instance Top₂ToRight₂  (n : Nat) [Top₂ n]   : Right₂ n := {}
+instance Bot₂ToTopSucc (n : Nat) [Bot₂ n]   : Top₂ n.succ := {}
 
-@[class] axiom Top (n : Nat) : Type
+class Top (n : Nat) : Type := (u : Unit := ())
 
-@[instance] axiom Top₁ToTop (n : Nat) [Top₁ n] : Top n
-@[instance] axiom Top₂ToTop (n : Nat) [Top₂ n] : Top n
+instance Top₁ToTop (n : Nat) [Top₁ n] : Top n := {}
+instance Top₂ToTop (n : Nat) [Top₂ n] : Top n := {}
 
 #synth Top Nat.zero.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ
diff --git a/tests/lean/run/typeclass_outparam.lean b/tests/lean/run/typeclass_outparam.lean
index 8f6d65f6ff..d05569c281 100644
--- a/tests/lean/run/typeclass_outparam.lean
+++ b/tests/lean/run/typeclass_outparam.lean
@@ -1,5 +1,5 @@
-@[class] axiom OPClass (α : outParam Type) (β : Type) : Type
+class OPClass (α : outParam Type) (β : Type) : Type := (u : Unit := ())
 
-@[instance] axiom op₁ : OPClass Nat Nat
+instance op₁ : OPClass Nat Nat := {}
 
 #synth OPClass Nat Nat