diff --git a/src/Lean/Server/Rpc/Deriving.lean b/src/Lean/Server/Rpc/Deriving.lean
index c0333cdea1..8ad3231d07 100644
--- a/src/Lean/Server/Rpc/Deriving.lean
+++ b/src/Lean/Server/Rpc/Deriving.lean
@@ -104,17 +104,15 @@ private def deriveStructureInstance (indVal : InductiveVal) (params : Array Expr
     -- helpers for type name syntax
     let paramIds ← params.mapM fun p => return mkIdent (← getFVarLocalDecl p).userName
     let typeId := Syntax.mkApp (← `(@$(mkIdent indVal.name))) paramIds
-    let packetId := mkIdent <| indVal.name ++ `RpcEncodingPacket
-    let packetAppliedId ← `($packetId ..)
     let instId := mkIdent (`_root_ ++ indVal.name.appendBefore "instRpcEncoding")
 
     `(variable $packetParamBinders* in
-      protected structure $packetId:ident where
+      structure RpcEncodingPacket where
         $[($fieldIds : $fieldEncTypeStxs)]*
         deriving FromJson, ToJson
 
       variable $(paramBinders ++ packetParamBinders ++ encInstBinders)* in
-      @[instance] def $instId := show RpcEncoding $typeId $packetAppliedId from {
+      @[instance] def $instId := show RpcEncoding $typeId (RpcEncodingPacket ..) from {
         rpcEncode := fun a => return { $[$encInits],* }
         rpcDecode := fun a => return { $[$decInits],* }
       }
@@ -133,7 +131,7 @@ private def deriveInductiveInstance (indVal : InductiveVal) (params : Array Expr
     (paramBinders packetParamBinders encInstBinders : Array (TSyntax ``Parser.Term.bracketedBinder)) : TermElabM Command := do
   trace[Elab.Deriving.RpcEncoding] "for inductive {indVal.name} with params {params}"
   withoutModifyingEnv do
-  let packetNm := indVal.name ++ `RpcEncodingPacket
+  let packetNm := (← `(RpcEncodingPacket)).1.getId
   addDecl <| .axiomDecl {
     name := packetNm
     levelParams := []
@@ -150,7 +148,7 @@ private def deriveInductiveInstance (indVal : InductiveVal) (params : Array Expr
       let tyStx ← PrettyPrinter.delab packetTp
       let name := (← getFVarLocalDecl arg).userName
       `(bracketedBinder| ($(mkIdent name) : $tyStx))
-    let pktCtor ← `(Parser.Command.ctor| | $(mkIdent ctor.getString!):ident $[$fieldStxs]* : $(mkIdent packetNm))
+    let pktCtor ← `(Parser.Command.ctor| | $(mkIdent ctor.getString!):ident $[$fieldStxs]* : RpcEncodingPacket)
 
     -- create encoder and decoder match arms
     let nms ← argVars.mapM fun _ => mkIdent <$> mkFreshBinderName
@@ -170,23 +168,22 @@ private def deriveInductiveInstance (indVal : InductiveVal) (params : Array Expr
   -- helpers for type name syntax
   let paramIds ← params.mapM fun p => return mkIdent (← getFVarLocalDecl p).userName
   let typeId := Syntax.mkApp (← `(@$(mkIdent indVal.name))) paramIds
-  let packetId ← `($(mkIdent packetNm) ..)
   let instId := mkIdent (`_root_ ++ indVal.name.appendBefore "instRpcEncoding")
 
   `(variable $packetParamBinders:bracketedBinder* in
-    protected inductive $(mkIdent packetNm) where
+    inductive RpcEncodingPacket where
       $[$(st.ctors):ctor]*
       deriving FromJson, ToJson
 
     variable $(paramBinders ++ packetParamBinders ++ encInstBinders)* in
-    @[instance] partial def $instId := show RpcEncoding $typeId $packetId from
+    @[instance] partial def $instId := show RpcEncoding $typeId (RpcEncodingPacket ..) from
       { rpcEncode, rpcDecode }
     where
-      rpcEncode {m} [Monad m] [MonadRpcSession m] (x : $typeId) : ExceptT String m $packetId :=
-        have inst : RpcEncoding $typeId $packetId := { rpcEncode, rpcDecode }
+      rpcEncode {m} [Monad m] [MonadRpcSession m] (x : $typeId) : ExceptT String m (RpcEncodingPacket ..) :=
+        have inst : RpcEncoding $typeId (RpcEncodingPacket ..) := { rpcEncode, rpcDecode }
         match x with $[$(st.encodes):matchAlt]*
-      rpcDecode {m} [Monad m] [MonadRpcSession m] (x : $packetId) : ExceptT String m $typeId :=
-        have inst : RpcEncoding $typeId $packetId := { rpcEncode, rpcDecode }
+      rpcDecode {m} [Monad m] [MonadRpcSession m] (x : RpcEncodingPacket ..) : ExceptT String m $typeId :=
+        have inst : RpcEncoding $typeId (RpcEncodingPacket ..) := { rpcEncode, rpcDecode }
         match x with $[$(st.decodes):matchAlt]*
   )
 
diff --git a/tests/lean/derivingRpcEncoding.lean b/tests/lean/derivingRpcEncoding.lean
index b971098f5d..4608ebbf6f 100644
--- a/tests/lean/derivingRpcEncoding.lean
+++ b/tests/lean/derivingRpcEncoding.lean
@@ -37,7 +37,6 @@ structure Bar where
   fooJson : FooJson
   deriving RpcEncoding, Inhabited
 
-#print Bar.RpcEncodingPacket
 #check instRpcEncodingBar
 #eval test Bar default
 
@@ -60,7 +59,6 @@ structure FooGeneric (α : Type) where
   b? : Option α
   deriving RpcEncoding, Inhabited
 
-#print FooGeneric.RpcEncodingPacket
 #check instRpcEncodingFooGeneric
 #eval test (FooGeneric Nat) default
 #eval test (FooGeneric Nat) { a := 3, b? := some 42 }
@@ -77,7 +75,6 @@ inductive FooInductive (α : Type) where
   | b : (n : Nat) → (a : α) → (m : Nat) → FooInductive α
   deriving RpcEncoding, Inhabited
 
-#print FooInductive.RpcEncodingPacket
 #check instRpcEncodingFooInductive
 #eval test (FooInductive BazInductive) (.a default default)
 #eval test (FooInductive BazInductive) (.b 42 default default)
@@ -86,8 +83,6 @@ inductive FooNested (α : Type) where
   | a : α → Array (FooNested α) → FooNested α
   deriving RpcEncoding, Inhabited
 
-#print FooNested.RpcEncodingPacket
-#check @FooNested.RpcEncodingPacket.a
 #eval test (FooNested BazInductive) (.a default #[default])
 
 inductive FooParam (n : Nat) where
@@ -100,7 +95,6 @@ inductive FooParam (n : Nat) where
 inductive Unused (α : Type) | a
   deriving RpcEncoding, Inhabited
 
-#print Unused.RpcEncodingPacket
 #check instRpcEncodingUnused
 structure NoRpcEncoding
 #eval test (Unused NoRpcEncoding) default
@@ -108,7 +102,6 @@ structure NoRpcEncoding
 structure UnusedStruct (α : Type)
   deriving RpcEncoding, Inhabited
 
-#print UnusedStruct.RpcEncodingPacket
 #check instRpcEncodingUnusedStruct
 #eval test (UnusedStruct NoRpcEncoding) default
 
diff --git a/tests/lean/derivingRpcEncoding.lean.expected.out b/tests/lean/derivingRpcEncoding.lean.expected.out
index f22d0a4a1a..281522e27f 100644
--- a/tests/lean/derivingRpcEncoding.lean.expected.out
+++ b/tests/lean/derivingRpcEncoding.lean.expected.out
@@ -1,57 +1,29 @@
 instRpcEncodingWithRpcRefFooRefRpcRef : RpcEncoding (WithRpcRef FooRef) Lsp.RpcRef
 ok: {"p": "0"}
-protected inductive Bar.RpcEncodingPacket : Type
-number of parameters: 0
-constructors:
-Bar.RpcEncodingPacket.mk : Lsp.RpcRef → FooJson → Bar.RpcEncodingPacket
-instRpcEncodingBar : RpcEncoding Bar Bar.RpcEncodingPacket
+instRpcEncodingBar : RpcEncoding Bar RpcEncodingPacket✝
 ok: {"fooRef": {"p": "0"}, "fooJson": {"s": ""}}
-instRpcEncodingBarTrans : RpcEncoding BarTrans BarTrans.RpcEncodingPacket
+instRpcEncodingBarTrans : RpcEncoding BarTrans RpcEncodingPacket✝
 ok: {"bar": {"fooRef": {"p": "0"}, "fooJson": {"s": ""}}}
-instRpcEncodingBaz : RpcEncoding Baz Baz.RpcEncodingPacket
+instRpcEncodingBaz : RpcEncoding Baz RpcEncodingPacket✝
 ok: {"arr": []}
-protected inductive FooGeneric.RpcEncodingPacket : Type → Type
-number of parameters: 1
-constructors:
-FooGeneric.RpcEncodingPacket.mk : {αPacket : Type} → αPacket → Option αPacket → FooGeneric.RpcEncodingPacket αPacket
 instRpcEncodingFooGeneric : (α αPacket : Type) →
-  [inst : RpcEncoding α αPacket] → RpcEncoding (FooGeneric α) (FooGeneric.RpcEncodingPacket αPacket)
+  [inst : RpcEncoding α αPacket] → RpcEncoding (FooGeneric α) (RpcEncodingPacket✝ αPacket)
 ok: {"a": 0}
 ok: {"b": 42, "a": 3}
-instRpcEncodingBazInductive : RpcEncoding BazInductive BazInductive.RpcEncodingPacket
+instRpcEncodingBazInductive : RpcEncoding BazInductive RpcEncodingPacket✝
 ok: {"baz":
  {"arr":
   [{"fooRef": {"p": "0"}, "fooJson": {"s": ""}},
    {"fooRef": {"p": "1"}, "fooJson": {"s": ""}}]}}
-protected inductive FooInductive.RpcEncodingPacket : Type → Type
-number of parameters: 1
-constructors:
-FooInductive.RpcEncodingPacket.a : {αPacket : Type} → αPacket → Lsp.RpcRef → FooInductive.RpcEncodingPacket αPacket
-FooInductive.RpcEncodingPacket.b : {αPacket : Type} → Nat → αPacket → Nat → FooInductive.RpcEncodingPacket αPacket
 instRpcEncodingFooInductive : (α αPacket : Type) →
-  [inst : RpcEncoding α αPacket] → RpcEncoding (FooInductive α) (FooInductive.RpcEncodingPacket αPacket)
+  [inst : RpcEncoding α αPacket] → RpcEncoding (FooInductive α) (RpcEncodingPacket✝ αPacket)
 ok: {"a": [{"baz": {"arr": []}}, {"p": "0"}]}
 ok: {"b": {"n": 42, "m": 0, "a": {"baz": {"arr": []}}}}
-protected inductive FooNested.RpcEncodingPacket : Type → Type
-number of parameters: 1
-constructors:
-FooNested.RpcEncodingPacket.a : {αPacket : Type} →
-  αPacket → Array (FooNested.RpcEncodingPacket αPacket) → FooNested.RpcEncodingPacket αPacket
-@FooNested.RpcEncodingPacket.a : {αPacket : Type} →
-  αPacket → Array (FooNested.RpcEncodingPacket αPacket) → FooNested.RpcEncodingPacket αPacket
 ok: {"a": [{"baz": {"arr": []}}, [{"a": [{"baz": {"arr": []}}, []]}]]}
-instRpcEncodingFooParam : (n : Nat) → RpcEncoding (FooParam n) FooParam.RpcEncodingPacket
+instRpcEncodingFooParam : (n : Nat) → RpcEncoding (FooParam n) RpcEncodingPacket✝
 ok: {"a": 42}
-protected inductive Unused.RpcEncodingPacket : Type
-number of parameters: 0
-constructors:
-Unused.RpcEncodingPacket.a : Unused.RpcEncodingPacket
-instRpcEncodingUnused : (α : Type) → RpcEncoding (Unused α) Unused.RpcEncodingPacket
+instRpcEncodingUnused : (α : Type) → RpcEncoding (Unused α) RpcEncodingPacket✝
 ok: "a"
-protected inductive UnusedStruct.RpcEncodingPacket : Type
-number of parameters: 0
-constructors:
-UnusedStruct.RpcEncodingPacket.mk : UnusedStruct.RpcEncodingPacket
-instRpcEncodingUnusedStruct : (α : Type) → RpcEncoding (UnusedStruct α) UnusedStruct.RpcEncodingPacket
+instRpcEncodingUnusedStruct : (α : Type) → RpcEncoding (UnusedStruct α) RpcEncodingPacket✝
 ok: {}
 Except.error "no inductive constructor matched"