diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/proof/single_core_proofs/scp_common.h b/Test/VeriFast/tasks/vTaskSwitchContext/proof/single_core_proofs/scp_common.h
index 1c3f72ec9..5923b6d89 100644
--- a/Test/VeriFast/tasks/vTaskSwitchContext/proof/single_core_proofs/scp_common.h
+++ b/Test/VeriFast/tasks/vTaskSwitchContext/proof/single_core_proofs/scp_common.h
@@ -14,8 +14,6 @@
  * All changes to the proofs, predicates, etc.
  * are guarded by a check that `VERIFAST_SINGLE_CORE` is 
  * NOT defined.
- * 
- * Temporary removals are guarded by `VERIFAST_TODO`.
  */
 
 
diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/proof/single_core_proofs/scp_list_predicates.h b/Test/VeriFast/tasks/vTaskSwitchContext/proof/single_core_proofs/scp_list_predicates.h
index 57c3c7fbf..43bb5142f 100644
--- a/Test/VeriFast/tasks/vTaskSwitchContext/proof/single_core_proofs/scp_list_predicates.h
+++ b/Test/VeriFast/tasks/vTaskSwitchContext/proof/single_core_proofs/scp_list_predicates.h
@@ -12,8 +12,6 @@
  * All changes to the proofs, predicates, etc.
  * are guarded by a check that `VERIFAST_SINGLE_CORE` is 
  * NOT defined.
- * 
- * Temporary removals are guarded by `VERIFAST_TODO`.
  */
 
 
@@ -736,7 +734,6 @@ lemma void remove_append<t>(t x, list<t> l1, list<t> l2)
 }
 @*/
 
-#endif /* VERIFAST_TODO */
 
 #endif /* SCP_LIST_PREDICATES_H */