diff --git a/src/Lean/Data/Lsp/Extra.lean b/src/Lean/Data/Lsp/Extra.lean
index 93bdfc7144..033b849763 100644
--- a/src/Lean/Data/Lsp/Extra.lean
+++ b/src/Lean/Data/Lsp/Extra.lean
@@ -69,14 +69,6 @@ structure PlainTermGoal where
 
 /-- An object which RPC clients can refer to without marshalling. -/
 abbrev RpcRef := USize
-inductive RpcValue where
-  | json : Json → RpcValue
-  | ref : RpcRef → RpcValue
-  deriving FromJson, ToJson, Inhabited
-
-inductive RpcValueKind where
-  | json | ref
-  deriving FromJson, ToJson
 
 /-- Initialize an RPC session at the given file's worker. -/
 structure RpcInitializeParams where
diff --git a/src/Lean/Server/FileWorker/Rpc.lean b/src/Lean/Server/FileWorker/Rpc.lean
index 9c05939409..ab462994ca 100644
--- a/src/Lean/Server/FileWorker/Rpc.lean
+++ b/src/Lean/Server/FileWorker/Rpc.lean
@@ -139,112 +139,3 @@ def registerRpcCallHandler (method : Name)
   rpcProcedures.modify fun ps => ps.insert method ⟨wrapper⟩
 
 end Lean.Server
-
-#exit -- TODO wrappers below
-
-namespace Lean.Server.Rpc
-open Lsp (RpcValueKind)
-
-/-- Like `RpcValue`, but with decoded `ref` IDs. -/
-inductive RpcInput where
-  | ref : IO.UntypedRef → RpcInput
-  | json : Json → RpcInput
-  deriving Inhabited
-open RpcInput
-
-private unsafe def RpcSession.decodePtrOrJson [Inhabited α] [FromJson α] : RpcInput → IO α
-  | ref r => r.getAsUnsafe α
-  | json j => match @fromJson? α _ j with
-    | Except.error e => throwThe IO.Error e
-    | Except.ok v => v
-
-private unsafe def RpcSession.decodePtr [Inhabited α] : RpcInput → IO α
-  | ref r => r.getAsUnsafe α
-  | json j => throwThe IO.Error "cannot decode, no FromJson instance"
-
-private def toRpcWrapperName (funcNm : Name) : Name :=
-  Name.mkStr funcNm "__rpc"
-
-open Elab Meta in
-private def wrapRpcFunc (funcId : Syntax) : Command.CommandElabM Unit := do
-  let env ← getEnv
-  let funcNm := funcId.getId
-  match env.find? funcNm with
-  | none      => throwError "unknown constant '{funcNm}'"
-  | some info =>
-    let cmds ← Command.liftTermElabM none do
-      forallTelescopeReducing info.type fun args retT => do
-        let mkFreshFVarName (arg : Expr) : TermElabM Name := do
-          let localDecl ← getLocalDecl arg.fvarId!
-          mkFreshUserName localDecl.userName.eraseMacroScopes
-
-        let hasInstance (cl : Name) (tp : Expr) : TermElabM Bool := do
-          let clTp ←
-            try mkAppM cl #[tp]
-            catch _ => throwError "failed to construct '{cl} {tp}'"
-          let inst? ← trySynthInstance clTp
-          inst? matches LOption.some _
-
-        -- (args : Array RpcInput) (retKind : RpcValueKind)
-        let rpcArgsId ← mkIdent <$> mkFreshUserName `args
-        let retKindArgId ← mkIdent <$> mkFreshUserName `retKind
-
-        let mut argTNames := #[]
-        let mut letIds := #[]
-        let mut decoders := #[]
-        let mut i := 0 -- enumerate? :(
-        for arg in args do
-          let argName ← mkFreshFVarName arg
-          let argT ← inferType arg
-          let some argTName ← argT.constName?
-            | throwError "non-constant type '{argT}'"
-          argTNames := argTNames.push <| mkIdent argTName
-          letIds := letIds.push <| mkIdent argName
-          -- a term to decode the `i`th argument
-          -- TODO add [FromJson α] for polymorphic arguments
-          let decoder ←
-            if (← hasInstance ``FromJson argT) then
-              `(Parser.Term.doExpr| RpcSession.decodePtrOrJson $rpcArgsId:ident[$(quote i)] )
-            else
-              `(Parser.Term.doExpr| RpcSession.decodePtr $rpcArgsId:ident[$(quote i)] )
-          decoders := decoders.push decoder
-          i := i+1
-
-        let rpcUnsafeId := mkIdent <| Name.mkStr funcNm "__rpc_unsafe"
-        let mkRetJson ←
-          if (← hasInstance ``ToJson retT) then
-            `(Parser.Term.doSeqIndent| pure <| RpcInput.json <| toJson <| @$funcId:ident $letIds*)
-          else
-            `(Parser.Term.doSeqIndent| throwThe IO.Error "cannot encode, no ToJson instance")
-        let cmd₁ ← `(
-          private unsafe def $rpcUnsafeId:ident ($rpcArgsId : Array RpcInput) ($retKindArgId : RpcValueKind)
-            : IO RpcInput := do
-            $[let $letIds:ident : $argTNames:ident ← $decoders]*
-            let ret ← @$funcId:ident $letIds*
-            let retJson ← match $retKindArgId:ident with
-              | RpcValueKind.ref => RpcInput.ref <$> IO.UntypedRef.mkRefUnsafe ret
-              | RpcValueKind.json => $mkRetJson
-            return retJson
-        )
-
-        let rpcId := mkIdent <| toRpcWrapperName funcNm
-        let cmd₂ ← `(
-          @[implementedBy $rpcUnsafeId:ident]
-          private constant $rpcId:ident ($rpcArgsId : Array RpcInput) ($retKindArgId : RpcValueKind)
-            : IO RpcInput
-        )
-
-        return #[cmd₁, cmd₂]
-    cmds.forM Command.elabCommand
-
-
-end Lean.Server.Rpc
-
-open Lean Elab Meta in
-elab "register_rpc_func" funcId:ident : command => do
-  Server.Rpc.wrapRpcFunc funcId
-  let funcNm := funcId.getId
-  let wrapperId := mkIdent <| Server.Rpc.toRpcWrapperName funcNm
-  let cmd ← `(
-    initialize Lean.Server.Rpc.registerRpcProcedure $(quote funcNm) ⟨$wrapperId:ident⟩)
-  Command.elabCommand cmd