fix: fixes #1848

src/Lean/Elab/Declaration.lean

@@ -190,7 +190,7 @@ def elabClassInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Uni
 def getTerminationHints (stx : Syntax) : TerminationHints :=
   let decl := stx[1]
   let k := decl.getKind
-  if k == ``Parser.Command.def || k == ``Parser.Command.theorem || k == ``Parser.Command.instance then
+  if k == ``Parser.Command.def || k == ``Parser.Command.abbrev || k == ``Parser.Command.theorem || k == ``Parser.Command.instance then
     let args := decl.getArgs
     { terminationBy? := args[args.size - 2]!.getOptional?, decreasingBy? := args[args.size - 1]!.getOptional? }
   else

src/Lean/Parser/Command.lean

@@ -101,7 +101,7 @@ def declVal          :=
   withAntiquot (mkAntiquot "declVal" `Lean.Parser.Command.declVal (isPseudoKind := true)) <|
     declValSimple <|> declValEqns <|> whereStructInst
 def «abbrev»         := leading_parser
-  "abbrev " >> declId >> ppIndent optDeclSig >> declVal
+  "abbrev " >> declId >> ppIndent optDeclSig >> declVal >> terminationSuffix
 def optDefDeriving   :=
   optional (atomic ("deriving " >> notSymbol "instance") >> sepBy1 ident ", ")
 def «def»            := leading_parser

tests/lean/run/1848.lean

@@ -0,0 +1,11 @@
+abbrev f : Nat → Nat
+  | 0 => 0
+  | n + 1 => f n
+termination_by _ n => n
+
+mutual
+abbrev f1 : Nat → Nat
+  | 0 => 0
+  | n + 1 => f1 n
+end
+termination_by _ n => n