diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v
index 6e66ef5cf70d6d2efca11b49435faa85a2bc1c74..9fe858a5b4a4c9eb8a4cfef4231fa2c24d051f87 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -65,13 +65,8 @@ Section join_handle.
     unfold join_inv. iApply @send_change_tid. done.
   Qed.
 
-  Global Instance join_handle_sync ty :
-    Sync (join_handle ty).
-  Proof.
-    iIntros (????) "**". (* FIXME: Why did it throw away the assumption we should have gotten? *)
-    done.
-  Qed.
-
+  Global Instance join_handle_sync ty : Sync (join_handle ty).
+  Proof. iIntros (????) "_ //". Qed.
 End join_handle.
 
 Section spawn.