diff --git a/iris/proofmode/string_ident.v b/iris/proofmode/string_ident.v
index 7e79a33c32fb4bc52d47c3d62e87bab0207d0796..422ca913e27a347d532e8c1a9106d49bfe2f064f 100644
--- a/iris/proofmode/string_ident.v
+++ b/iris/proofmode/string_ident.v
@@ -80,15 +80,5 @@ by ident [id] into the name given by string [s]. *)
 Ltac rename_by_string id s :=
   StringToIdent.string_to_ident_cps s ltac:(fun x => rename id into x).
 
-(** We can also use this to write Ltac that *returns* the desired ident.
-However, this function will produce wrong results under [Set Mangle Names], so
-use with caution. *)
-Ltac string_to_ident s :=
-  let s := (eval cbv in s) in
-  let x := constr:(ltac:(clear; (* needed since s might already be in scope
-                         where this is called *)
-                         StringToIdent.string_to_ident_cps s ltac:(fun x => intros x);
-                         exact tt) : unit -> unit) in
-  match x with
-  | (fun (name:_) => _) => name
-  end.
+(* We also directly expose the CPS primitive. *)
+Ltac string_to_ident_cps := StringToIdent.string_to_ident_cps.
diff --git a/tests/string_ident.v b/tests/string_ident.v
index dc22df6de751ac4f66c2f003313a062f3ba7889c..5313a51b88d9d4c721e7594bfb4e817e84a28c5a 100644
--- a/tests/string_ident.v
+++ b/tests/string_ident.v
@@ -32,7 +32,7 @@ Lemma test_string_to_ident_not_fresh (n:nat) : ∀ (n:nat), nat.
 Proof.
   (* we want to check that this [string_to_ident "n"] call succeeds even with
   [n] in the context *)
-  let x := string_to_ident "n" in
+  string_to_ident_cps "n" ltac:(fun x =>
   let x := fresh x in
-  intros x.
+  intros x).
 Abort.