diff --git a/proof/invariant-abstract/Syscall_AI.thy b/proof/invariant-abstract/Syscall_AI.thy
index 4c66515e52..3b5e6c0e65 100644
--- a/proof/invariant-abstract/Syscall_AI.thy
+++ b/proof/invariant-abstract/Syscall_AI.thy
@@ -1146,8 +1146,6 @@ lemma hy_inv: "(\<And>s f. P (trans_state f s) = P s) \<Longrightarrow> \<lbrace
   apply (wp | simp)+
   done
 
-declare hoare_seq_ext[wp]
-
 lemma ct_active_simple [elim!]:
   "ct_active s \<Longrightarrow> st_tcb_at simple (cur_thread s) s"
   by (fastforce simp: ct_in_state_def elim!: pred_tcb_weakenE)