Regenerate the code

1 files changed, 2 insertions, 6 deletions

diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean
index 2112e282..5f9ec0f2 100644
--- a/tests/lean/NoNestedBorrows.lean
+++ b/tests/lean/NoNestedBorrows.lean
@@ -487,9 +487,7 @@ def id_mut_pair1
   (T1 T2 : Type) (x : T1) (y : T2) :
   Result ((T1 × T2) × ((T1 × T2) → Result (T1 × T2)))
   :=
-  let back_'a := fun ret => let (t, t1) := ret
-                            Result.ret (t, t1)
-  Result.ret ((x, y), back_'a)
+  Result.ret ((x, y), Result.ret)
 
 /- [no_nested_borrows::id_mut_pair2]:
    Source: 'src/no_nested_borrows.rs', lines 418:0-418:88 -/
@@ -498,9 +496,7 @@ def id_mut_pair2
   Result ((T1 × T2) × ((T1 × T2) → Result (T1 × T2)))
   :=
   let (t, t1) := p
-  let back_'a := fun ret => let (t2, t3) := ret
-                            Result.ret (t2, t3)
-  Result.ret ((t, t1), back_'a)
+  Result.ret ((t, t1), Result.ret)
 
 /- [no_nested_borrows::id_mut_pair3]:
    Source: 'src/no_nested_borrows.rs', lines 422:0-422:93 -/