diff --git a/docs/user-guide/src/tour/peek.md b/docs/user-guide/src/tour/peek.md
index 19bccb4e764..b997b77106b 100644
--- a/docs/user-guide/src/tour/peek.md
+++ b/docs/user-guide/src/tour/peek.md
@@ -3,7 +3,7 @@
 > **Recommended reading:** 
 > [3.3: Peek](https://rust-unofficial.github.io/too-many-lists/second-peek.html)
 
-Ideally, we could implement `peek` and `try_peek` like we implemented `pop` and `try_pop` before. Like `pop`, `push` can only be called if the list is non-empty, and it then always returns a reference to the element at the head of the list (type `&T`). Similarly, `try_peek` can be called on any list, but returns an `Option<&T>`. The latter is currently not possible in Prusti, since structures containing references are not supported at the moment.
+Ideally, we could implement `peek` and `try_peek` like we implemented `pop` and `try_pop` before. Like `pop`, `peek` can only be called if the list is non-empty, and it then always returns a reference to the element at the head of the list (type `&T`). Similarly, `try_peek` can be called on any list, but returns an `Option<&T>`. The latter is currently not possible in Prusti, since structures containing references are not supported at the moment.
 
 <!-- TODO: link capabilities/limitations chapter (refs in structs) -->
 
@@ -27,4 +27,4 @@ Here you can see the full code we have now:
 ```rust,noplaypen
 // Expand to see full code up to this chapter
 {{#rustdoc_include ../../../../prusti-tests/tests/verify/pass/user-guide/peek.rs:nothing}}
-```
\ No newline at end of file
+```
diff --git a/docs/user-guide/src/verify/panic.md b/docs/user-guide/src/verify/panic.md
index c93970d88eb..b2d12fc4683 100644
--- a/docs/user-guide/src/verify/panic.md
+++ b/docs/user-guide/src/verify/panic.md
@@ -22,7 +22,7 @@ error[P0004]: unreachable!(..) statement might be reachable
 This message correctly points out that the `unreachable!()` statement might actually be reachable.
 
 The message says "might" because Prusti is conservative, i.e., it reports a verification error *unless* it can prove that the statement is unreachable.
-Hence, Prusti successfully the example below as it can rule out that the condition in the conditional statement, `a <= 0`, holds.
+Hence, Prusti successfully verified the example below as it can rule out that the condition in the conditional statement, `a <= 0`, holds.
 
 ```rust,noplaypen,ignore
 pub fn main() {
diff --git a/prusti-tests/tests/verify/pass/user-guide/peek_mut_pledges.rs b/prusti-tests/tests/verify/pass/user-guide/peek_mut_pledges.rs
index e083b676514..659eae96dcf 100644
--- a/prusti-tests/tests/verify/pass/user-guide/peek_mut_pledges.rs
+++ b/prusti-tests/tests/verify/pass/user-guide/peek_mut_pledges.rs
@@ -218,6 +218,7 @@ mod prusti_tests {
         prusti_assert!(*list.peek() == 16);
     }
 
+    //// ANCHOR: test_peek_mut
     fn _test_peek_mut() {
         let mut list = List::new();
         list.push(8);
@@ -238,4 +239,5 @@ mod prusti_tests {
         prusti_assert!(*list.lookup(0) == 5); // slot 0 is now `5`
         prusti_assert!(*list.lookup(1) == 8); // slot 1 is unchanged
     }
-}
\ No newline at end of file
+    //// ANCHOR_END: test_peek_mut
+}