diff --git a/library/init/lean/elaborator/basic.lean b/library/init/lean/elaborator/basic.lean
index deeb89fa2c..be90f88c2e 100644
--- a/library/init/lean/elaborator/basic.lean
+++ b/library/init/lean/elaborator/basic.lean
@@ -406,6 +406,12 @@ namespace Elab
 instance {α} : Inhabited (Elab α) :=
 ⟨fun _ => default _⟩
 
+def mkFreshName : Elab Name :=
+do s ← get;
+   let n := s.ngen.curr;
+   modify $ fun s => { ngen := s.ngen.next, .. s };
+   pure n
+
 def getScope : Elab ElabScope :=
 do s ← get; pure s.scopes.head
 
diff --git a/library/init/lean/elaborator/preterm.lean b/library/init/lean/elaborator/preterm.lean
index d9887cf8c5..0dacabc8e9 100644
--- a/library/init/lean/elaborator/preterm.lean
+++ b/library/init/lean/elaborator/preterm.lean
@@ -118,5 +118,18 @@ fun n => do
    else
      pure $ Expr.sort level
 
+@[builtinPreTermElab «arrow»] def convertArrow : PreTermElab :=
+fun n => do
+  id ← mkFreshName;
+  dom ← toPreTerm $ n.getArg 0;
+  rng ← toPreTerm $ n.getArg 2;
+  pure $ Expr.pi id BinderInfo.default dom rng
+
+@[builtinPreTermElab «hole»] def convertHole : PreTermElab :=
+fun _ => pure $ Expr.mvar Name.anonymous
+
+@[builtinPreTermElab «sorry»] def convertSorry : PreTermElab :=
+fun _ => pure $ Expr.app (Expr.const `sorryAx []) (Expr.mvar Name.anonymous)
+
 end Elab
 end Lean
diff --git a/library/init/lean/namegenerator.lean b/library/init/lean/namegenerator.lean
index 3c48b4928e..30bdb3cbaa 100644
--- a/library/init/lean/namegenerator.lean
+++ b/library/init/lean/namegenerator.lean
@@ -16,8 +16,11 @@ namespace NameGenerator
 
 instance : Inhabited NameGenerator := ⟨{}⟩
 
-def next (g : NameGenerator) : Name × NameGenerator :=
-(Name.mkNumeral g.namePrefix g.idx, { idx := g.idx + 1, .. g })
+def curr (g : NameGenerator) : Name :=
+Name.mkNumeral g.namePrefix g.idx
+
+def next (g : NameGenerator) : NameGenerator :=
+{ idx := g.idx + 1, .. g }
 
 def mkChild (g : NameGenerator) : NameGenerator × NameGenerator :=
 ({ namePrefix := Name.mkNumeral g.namePrefix g.idx, idx := 1 },