diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index fec4f33a7c..c3100e0296 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -31,9 +31,10 @@ def terminationHint1 (p : Parser) := leading_parser p
 def terminationHint (p : Parser) := terminationHintMany p <|> terminationHint1 p
 
 def terminationBy := leading_parser "termination_by " >> terminationHint termParser
+def terminationByCore := leading_parser "termination_by' " >> terminationHint termParser
 def decreasingBy := leading_parser "decreasing_by " >> terminationHint Tactic.tacticSeq
 
-def terminationSuffix := optional terminationBy >> optional decreasingBy
+def terminationSuffix := optional (terminationBy <|> terminationByCore) >> optional decreasingBy
 
 @[builtinCommandParser]
 def moduleDoc := leading_parser ppDedent $ "/-!" >> commentBody >> ppLine