diff --git a/src/Lean/Elab/PreDefinition/Structural/Main.lean b/src/Lean/Elab/PreDefinition/Structural/Main.lean
index 1ef5fdd13a..6379398d1a 100644
--- a/src/Lean/Elab/PreDefinition/Structural/Main.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/Main.lean
@@ -84,10 +84,10 @@ def structuralRecursion (preDefs : Array PreDefinition) : TermElabM Unit :=
     let preDefNonRec ← eraseRecAppSyntax preDefNonRec
     let preDef ← eraseRecAppSyntax preDefs[0]
     state.addMatchers.forM liftM
+    registerEqnsInfo preDef recArgPos
     mapError (addNonRec preDefNonRec) (fun msg => m!"structural recursion failed, produced type incorrect term{indentD msg}")
     addAndCompilePartialRec #[preDef]
     addSmartUnfoldingDef preDef recArgPos
-    registerEqnsInfo preDef recArgPos
 
 builtin_initialize
   registerTraceClass `Elab.definition.structural
diff --git a/tests/lean/run/simpAtDefIssue.lean b/tests/lean/run/simpAtDefIssue.lean
new file mode 100644
index 0000000000..e82f81f901
--- /dev/null
+++ b/tests/lean/run/simpAtDefIssue.lean
@@ -0,0 +1,11 @@
+@[simp] def g (x y : Nat) : Nat :=
+  match x, y with
+  | 0,   0 => 1
+  | 0,   y => y
+  | x+1, 5 => 2 * g x 0
+  | x+1, y => 2 * g x y
+
+#check g._eq_1
+#check g._eq_2
+#check g._eq_3
+#check g._eq_4