diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean
index b8073722b9..f1cf91a4fc 100644
--- a/src/Lean/Elab/Declaration.lean
+++ b/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
diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index bb61fbcc34..35af9ce35a 100644
--- a/src/Lean/Parser/Command.lean
+++ b/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
diff --git a/tests/lean/run/1848.lean b/tests/lean/run/1848.lean
new file mode 100644
index 0000000000..a59b1bdeb9
--- /dev/null
+++ b/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