diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 433a4be18c..e7e1ab8f5c 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -244,6 +244,13 @@ stx.isAntiquot || stx.isIdent
 @[builtinTermParser] def byTactic    := parser!:maxPrec "by " >> Tactic.nonEmptySeq
 
 @[builtinTermParser] def funBinder.quot : Parser := parser! "`(funBinder|"  >> toggleInsideQuot funBinder >> ")"
+
+@[builtinTermParser] def panic       := parser!:leadPrec "panic! " >> termParser
+@[builtinTermParser] def unreachable := parser!:leadPrec "unreachable! " >> termParser
+@[builtinTermParser] def dbgTrace    := parser!:leadPrec "dbgTrace! " >> termParser >> "; " >> termParser
+@[builtinTermParser] def assert      := parser!:leadPrec "assert! " >> termParser >> "; " >> termParser
+@[builtinTermParser] def «return»    := parser!:leadPrec "return " >> termParser
+
 end Term
 
 -- Use `unboxSingleton` trick similar to the one used at Command.lean for `Term.quot`