diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean
index 3d24e3fefc..a54bfcc96e 100644
--- a/src/Lean/Elab/Inductive.lean
+++ b/src/Lean/Elab/Inductive.lean
@@ -439,15 +439,12 @@ adaptReader (fun (ctx : Term.Context) => { ctx with levelNames := allUserLevelNa
       | Except.ok levelParams => do
         indTypes ← replaceIndFVarsWithConsts views indFVars levelParams numParams indTypes;
         let indTypes := applyInferMod views numParams indTypes;
-        traceIndTypes indTypes;
         pure $ Declaration.inductDecl levelParams numParams indTypes isUnsafe
 
 def elabInductiveCore (views : Array InductiveView) : CommandElabM Unit := do
 let view0 := views.get! 0;
 decl ← runTermElabM view0.declName $ fun vars => mkInductiveDecl vars views;
--- TODO register decl
-pure ()
-
+addDecl view0.ref decl
 
 end Command
 end Elab
diff --git a/tests/lean/inductive1.lean b/tests/lean/inductive1.lean
index 3acfe1030d..fd88603a1b 100644
--- a/tests/lean/inductive1.lean
+++ b/tests/lean/inductive1.lean
@@ -106,3 +106,13 @@ inductive T1 : Nat → Type
 
 inductive T1 : Nat → Type
 | z1 : Nat -- unexpected constructor resulting type
+
+
+-- Test13
+
+inductive A (α : Type u) (β : Type v)
+| nil {}
+| protected cons : α → β → A → A
+
+open A
+#check cons -- unknown `cons`, it is protected
diff --git a/tests/lean/inductive1.lean.expected.out b/tests/lean/inductive1.lean.expected.out
index 65fe30abe4..cc7626d8eb 100644
--- a/tests/lean/inductive1.lean.expected.out
+++ b/tests/lean/inductive1.lean.expected.out
@@ -26,3 +26,5 @@ inductive1.lean:105:0: error: unexpected constructor resulting type, type expect
   T1
 inductive1.lean:108:0: error: unexpected constructor resulting type
   Nat
+inductive1.lean:118:7: error: unknown identifier 'cons'
+(sorryAx ?m_1) : ?m_1
diff --git a/tests/lean/run/inductive1.lean b/tests/lean/run/inductive1.lean
new file mode 100644
index 0000000000..cf3cf9b638
--- /dev/null
+++ b/tests/lean/run/inductive1.lean
@@ -0,0 +1,45 @@
+new_frontend
+
+inductive L1.{u} (α : Type u)
+| nil
+| cons : α → L1 → L1
+
+#check L1
+#check @L1.cons
+
+inductive L2.{u} (α : Type u)
+| nil
+| cons (head : α) (tail : L2)
+
+#check @L2.cons
+
+universes u v
+variable (α : Type u)
+
+inductive A (β : Type v)
+| nil {}
+| protected cons : α → β → A → A
+
+#check @A.cons
+#check A.nil Nat Bool
+
+mutual
+  inductive isEven : Nat → Prop
+  | z : isEven 0
+  | s (n : Nat) : isOdd n → isEven (n+1)
+
+  inductive isOdd : Nat → Prop
+  | s (n : Nat) : isEven n → isOdd (n+1)
+end
+
+#check isEven
+#check isOdd.s
+#check @isEven.rec
+
+inductive V (α : Type _) : Nat → Type _
+| nil  : V 0
+| cons {n : Nat} : α → V n → V (n+1)
+
+#check @V.nil
+#check @V.cons
+#check @V.rec