diff --git a/Qpf/Macro/Data.lean b/Qpf/Macro/Data.lean
index fa1a9ca..1ea2a1b 100644
--- a/Qpf/Macro/Data.lean
+++ b/Qpf/Macro/Data.lean
@@ -6,7 +6,6 @@ import Qpf.Macro.Data.Replace
 import Qpf.Macro.Data.Count
 import Qpf.Macro.Data.View
 import Qpf.Macro.Data.Ind
-import Qpf.Macro.NameUtils
 import Qpf.Macro.Common
 import Qpf.Macro.Comp
 
@@ -66,7 +65,7 @@ open Elab.Term (TermElabM)
 
 
 def CtorView.declReplacePrefix (pref new_pref : Name) (ctor: CtorView) : CtorView :=
-  let declName := Name.replacePrefix2 pref new_pref ctor.declName
+  let declName := Name.replacePrefix ctor.declName pref new_pref 
   {
     declName,
     ref := ctor.ref
@@ -113,7 +112,7 @@ def mkHeadT (view : InductiveView) : CommandElabM Name := do
   }
   -- The head type is the same as the original type, but with all constructor arguments removed
   let ctors ← view.ctors.mapM fun ctor => do
-    let declName := Name.replacePrefix2 view.declName declName ctor.declName
+    let declName := ctor.declName.replacePrefix view.declName declName 
     pure {
       modifiers, declName,
       ref := ctor.ref
@@ -157,7 +156,7 @@ def mkChildT (view : InductiveView) (r : Replace) (headTName : Name) : CommandEl
   let target_type := Syntax.mkApp (mkIdent ``TypeVec) #[quote r.arity]
 
   let matchAlts ← view.ctors.mapM fun ctor => do
-    let head := mkIdent $ Name.replacePrefix2 view.declName headTName ctor.declName
+    let head := Lean.mkIdent (ctor.declName.replacePrefix view.declName headTName)
 
     let counts := countVarOccurences r ctor.type?
     let counts := counts.map fun n =>
@@ -221,7 +220,7 @@ def mkQpf (shapeView : InductiveView) (ctorArgs : Array CtorArgs) (headT P : Ide
   let boxBody ← ctors.mapM fun (ctor, args) => do
     let argsId  := args.args.map mkIdent
     let alt     := mkIdent ctor.declName
-    let headAlt := mkIdent $ Name.replacePrefix2 shapeView.declName headT.getId ctor.declName
+    let headAlt := mkIdent $ ctor.declName.replacePrefix shapeView.declName headT.getId 
 
     `(matchAltExpr| | $alt:ident $argsId:ident* => ⟨$headAlt:ident, fun i => match i with
         $(
@@ -258,7 +257,7 @@ def mkQpf (shapeView : InductiveView) (ctorArgs : Array CtorArgs) (headT P : Ide
   let unbox_child := mkIdent <|<- Elab.Term.mkFreshBinderName;
   let unboxBody ← ctors.mapM fun (ctor, args) => do
     let alt     := mkIdent ctor.declName
-    let headAlt := mkIdent $ Name.replacePrefix2 shapeView.declName headT.getId ctor.declName
+    let headAlt := mkIdent $ ctor.declName.replacePrefix shapeView.declName headT.getId
 
     let args : Array Term ← args.args.mapM fun arg => do
       -- find the pair `(i, j)` such that the argument is the `j`-th occurence of the `i`-th type
diff --git a/Qpf/Macro/Data/Constructors.lean b/Qpf/Macro/Data/Constructors.lean
index c97d5fd..f431fa1 100644
--- a/Qpf/Macro/Data/Constructors.lean
+++ b/Qpf/Macro/Data/Constructors.lean
@@ -1,7 +1,6 @@
 import Qpf.Macro.Data.Replace
 import Qpf.Macro.Data.RecForm
 import Qpf.Macro.Data.View
-import Qpf.Macro.NameUtils
 
 open Lean Meta Elab Elab.Command 
 open PrettyPrinter (delab)
@@ -31,7 +30,7 @@ def mkConstructorsWithNameAndType
     let args := args.toArray
 
     let mk := mkIdent ((DataCommand.fixOrCofix view.command).getId ++ `mk)
-    let shapeCtor := mkIdent <| Name.replacePrefix2 view.declName shape ctor.declName
+    let shapeCtor := mkIdent <| Name.replacePrefix ctor.declName view.declName shape
     trace[QPF] "shapeCtor = {shapeCtor}"
 
 
@@ -70,7 +69,7 @@ def mkConstructorsWithNameAndType
 -/
 def mkConstructors (view : DataView) (shape : Name) : CommandElabM Unit := do
   let explicit ← view.getExplicitExpectedType
-  let nameGen := (mkIdent <| Name.stripPrefix2 (←getCurrNamespace) ·.declName)
+  let nameGen := (mkIdent <| ·.declName.replacePrefix (←getCurrNamespace) .anonymous)
 
   mkConstructorsWithNameAndType view shape nameGen explicit explicit #[]
 
diff --git a/Qpf/Macro/NameUtils.lean b/Qpf/Macro/NameUtils.lean
deleted file mode 100644
index c9bddfc..0000000
--- a/Qpf/Macro/NameUtils.lean
+++ /dev/null
@@ -1,17 +0,0 @@
-open Lean Meta
-
-namespace Lean.Name
--- This function has diffreent behaviour from Name.replacePrefix
-def replacePrefix2 (old_pref new_pref : Name) : Name → Name
-  | Name.anonymous => Name.anonymous
-  | Name.str p s   => let p' := if p == old_pref then new_pref
-                                else replacePrefix2 old_pref new_pref p
-                      Name.mkStr p' s
-  | Name.num p v   => let p' := if p == old_pref then new_pref
-                                else replacePrefix2 old_pref new_pref p
-                      Name.mkNum p' v
-
-
-def stripPrefix2 (old_pref : Name) : Name → Name
-  := Name.replacePrefix2 old_pref .anonymous
-end Lean.Name