diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 76433d1dc8..c058c71625 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -170,6 +170,9 @@ def letRecDecls      := sepBy1 (group (optional «attributes» >> letDecl)) ", "
 @[builtinTermParser] def nativeDecide := parser! "nativeDecide! " >> termParser maxPrec
 @[builtinTermParser] def decide       := parser! "decide! " >> termParser maxPrec
 
+@[builtinTermParser] def typeOf       := parser! "typeOf! " >> termParser maxPrec
+@[builtinTermParser] def ensureTypeOf := parser! "ensureTypeOf! " >> termParser maxPrec >> strLit >> termParser
+
 @[builtinTermParser] def not    := parser! "¬" >> termParser 40
 @[builtinTermParser] def bnot   := parser! "!" >> termParser 40
 -- symbol precedence should be higher, but must match the one of `sub` below