diff --git a/src/Init/Lean/Elaborator/Command.lean b/src/Init/Lean/Elaborator/Command.lean
index 645ca27b99..041e585b2d 100644
--- a/src/Init/Lean/Elaborator/Command.lean
+++ b/src/Init/Lean/Elaborator/Command.lean
@@ -190,14 +190,6 @@ fun n => do
   runIO (IO.println (toString pos ++ " " ++ toString resolvedIds));
   pure ()
 
-@[builtinCommandElab «preterm»] def elabPreTerm : CommandElab :=
-fun n => do
-  let s := n.getArg 1;
-  runIO (IO.println s);
-  pre ← toPreTerm (s.lift Expr);
-  runIO (IO.println pre.dbgToString);
-  pure ()
-
 @[builtinCommandElab «elab»] def elabElab : CommandElab :=
 fun n => do
   let s := n.getArg 1;
diff --git a/src/Init/Lean/Parser/Command.lean b/src/Init/Lean/Parser/Command.lean
index 3906d4521d..daa211096d 100644
--- a/src/Init/Lean/Parser/Command.lean
+++ b/src/Init/Lean/Parser/Command.lean
@@ -82,7 +82,6 @@ declModifiers >> («abbrev» <|> «def» <|> «theorem» <|> «constant» <|> «
 @[builtinCommandParser] def check          := parser! "#check " >> termParser
 @[builtinCommandParser] def exit           := parser! "#exit"
 @[builtinCommandParser] def «resolve_name» := parser! "#resolve_name " >> ident
-@[builtinCommandParser] def «preterm»      := parser! "#preterm " >> termParser
 @[builtinCommandParser] def «elab»         := parser! "#elab " >> termParser
 @[builtinCommandParser] def «init_quot»    := parser! "init_quot"
 @[builtinCommandParser] def «set_option»   := parser! "set_option " >> ident >> (symbolOrIdent "true" <|> symbolOrIdent "false" <|> strLit <|> numLit)