diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean
index 0bb2c5dd86..ce899f19f5 100644
--- a/src/Init/Meta.lean
+++ b/src/Init/Meta.lean
@@ -1518,26 +1518,33 @@ end Syntax
 
 namespace TSyntax
 
-def expandInterpolatedStrChunks (chunks : Array Syntax) (mkAppend : Syntax → Syntax → MacroM Syntax) (mkElem : Syntax → MacroM Syntax) : MacroM Syntax := do
+def expandInterpolatedStrChunks (chunks : Array Syntax) (mkAppend : Syntax → Syntax → MacroM Syntax)
+  (mkElem : Syntax → MacroM Syntax) (mkLit : String → MacroM Syntax) : MacroM Syntax := do
   let mut result := Syntax.missing
   for elem in chunks do
     let elem ← match elem.isInterpolatedStrLit? with
       | none     => withRef elem <| mkElem elem
       | some str =>
         if String.Internal.isEmpty str then continue
-        else withRef elem <| mkElem (Syntax.mkStrLit str)
+        else withRef elem <| mkLit str
     if result.isMissing then
       result := elem
     else
       result ← mkAppend result elem
   if result.isMissing then
-    mkElem (Syntax.mkStrLit "")
+    mkLit ""
   else
     return result
 
 open TSyntax.Compat in
-def expandInterpolatedStr (interpStr : TSyntax interpolatedStrKind) (type : Term) (toTypeFn : Term) : MacroM Term := do
-  let r ← expandInterpolatedStrChunks interpStr.raw.getArgs (fun a b => `($a ++ $b)) (fun a => `($toTypeFn $a))
+/-- Expand `interpStr` into a term of type `type` (which supports ` ++ `),
+calling `ofInterpFn` on terms within `{}`,
+and `ofLitFn` on the literals between the interpolations. -/
+def expandInterpolatedStr (interpStr : TSyntax interpolatedStrKind) (type : Term) (ofInterpFn : Term) (ofLitFn : Term := ofInterpFn) : MacroM Term := do
+  let r ← expandInterpolatedStrChunks interpStr.raw.getArgs
+    (fun a b => `($a ++ $b))
+    (fun a => `($ofInterpFn $a))
+    (fun s => `($ofLitFn $(Syntax.mkStrLit s)))
   `(($r : $type))
 
 def getDocString (stx : TSyntax `Lean.Parser.Command.docComment) : String :=