diff --git a/lib/Monads/More_NonDetMonadVCG.thy b/lib/Monads/More_NonDetMonadVCG.thy
index 4ab291159..9c98b6ed5 100644
--- a/lib/Monads/More_NonDetMonadVCG.thy
+++ b/lib/Monads/More_NonDetMonadVCG.thy
@@ -426,8 +426,6 @@ lemma hoare_Ball_helper:
   apply (rule refl)
   done
 
-lemmas hoare_gets_post = hoare_gets_sp (* FIXME lib: eliminate *)
-
 lemma handy_prop_divs:
   assumes x: "\<And>P. \<lbrace>\<lambda>s. P (Q s) \<and> S s\<rbrace> f \<lbrace>\<lambda>rv s. P (Q' rv s)\<rbrace>"
              "\<And>P. \<lbrace>\<lambda>s. P (R s) \<and> S s\<rbrace> f \<lbrace>\<lambda>rv s. P (R' rv s)\<rbrace>"
diff --git a/proof/crefine/ARM/ArchMove_C.thy b/proof/crefine/ARM/ArchMove_C.thy
index 6dcd98e18..dccb362a3 100644
--- a/proof/crefine/ARM/ArchMove_C.thy
+++ b/proof/crefine/ARM/ArchMove_C.thy
@@ -65,7 +65,7 @@ lemma setCTE_asidpool':
   "\<lbrace> ko_at' (ASIDPool pool) p \<rbrace> setCTE c p' \<lbrace>\<lambda>_. ko_at' (ASIDPool pool) p\<rbrace>"
   apply (clarsimp simp: setCTE_def)
   apply (simp add: setObject_def split_def)
-  apply (rule hoare_seq_ext [OF _ hoare_gets_post])
+  apply (rule hoare_seq_ext [OF _ hoare_gets_sp])
   apply (clarsimp simp: valid_def in_monad)
   apply (frule updateObject_type)
   apply (clarsimp simp: obj_at'_def projectKOs)
diff --git a/proof/crefine/ARM_HYP/ArchMove_C.thy b/proof/crefine/ARM_HYP/ArchMove_C.thy
index 98346790a..047455718 100644
--- a/proof/crefine/ARM_HYP/ArchMove_C.thy
+++ b/proof/crefine/ARM_HYP/ArchMove_C.thy
@@ -146,7 +146,7 @@ lemma setCTE_asidpool':
   "\<lbrace> ko_at' (ASIDPool pool) p \<rbrace> setCTE c p' \<lbrace>\<lambda>_. ko_at' (ASIDPool pool) p\<rbrace>"
   apply (clarsimp simp: setCTE_def)
   apply (simp add: setObject_def split_def)
-  apply (rule hoare_seq_ext [OF _ hoare_gets_post])
+  apply (rule hoare_seq_ext [OF _ hoare_gets_sp])
   apply (clarsimp simp: valid_def in_monad)
   apply (frule updateObject_type)
   apply (clarsimp simp: obj_at'_def projectKOs)
diff --git a/proof/crefine/RISCV64/VSpace_C.thy b/proof/crefine/RISCV64/VSpace_C.thy
index 8589e90f6..ea61317bf 100644
--- a/proof/crefine/RISCV64/VSpace_C.thy
+++ b/proof/crefine/RISCV64/VSpace_C.thy
@@ -1531,7 +1531,7 @@ lemma setCTE_asidpool':
   "\<lbrace> ko_at' (ASIDPool pool) p \<rbrace> setCTE c p' \<lbrace>\<lambda>_. ko_at' (ASIDPool pool) p\<rbrace>"
   apply (clarsimp simp: setCTE_def)
   apply (simp add: setObject_def split_def)
-  apply (rule hoare_seq_ext [OF _ hoare_gets_post])
+  apply (rule hoare_seq_ext [OF _ hoare_gets_sp])
   apply (clarsimp simp: valid_def in_monad)
   apply (frule updateObject_type)
   apply (clarsimp simp: obj_at'_def)
diff --git a/proof/crefine/X64/VSpace_C.thy b/proof/crefine/X64/VSpace_C.thy
index f0e230674..3957abb1a 100644
--- a/proof/crefine/X64/VSpace_C.thy
+++ b/proof/crefine/X64/VSpace_C.thy
@@ -2231,7 +2231,7 @@ lemma setCTE_asidpool':
   "\<lbrace> ko_at' (ASIDPool pool) p \<rbrace> setCTE c p' \<lbrace>\<lambda>_. ko_at' (ASIDPool pool) p\<rbrace>"
   apply (clarsimp simp: setCTE_def)
   apply (simp add: setObject_def split_def)
-  apply (rule hoare_seq_ext [OF _ hoare_gets_post])
+  apply (rule hoare_seq_ext [OF _ hoare_gets_sp])
   apply (clarsimp simp: valid_def in_monad)
   apply (frule updateObject_type)
   apply (clarsimp simp: obj_at'_def projectKOs)
diff --git a/proof/refine/ARM/KHeap_R.thy b/proof/refine/ARM/KHeap_R.thy
index a946d12c3..f20b2e8f5 100644
--- a/proof/refine/ARM/KHeap_R.thy
+++ b/proof/refine/ARM/KHeap_R.thy
@@ -186,7 +186,7 @@ lemma obj_at_setObject1:
    setObject p (v::'a::pspace_storable)
   \<lbrace> \<lambda>rv. obj_at' (\<lambda>x::'a::pspace_storable. True) t \<rbrace>"
   apply (simp add: setObject_def split_def)
-  apply (rule hoare_seq_ext [OF _ hoare_gets_post])
+  apply (rule hoare_seq_ext [OF _ hoare_gets_sp])
   apply (clarsimp simp: valid_def in_monad obj_at'_def
                         projectKOs lookupAround2_char1
                         project_inject
@@ -208,7 +208,7 @@ lemma obj_at_setObject2:
    setObject p (v::'a)
   \<lbrace> \<lambda>rv. obj_at' P t \<rbrace>"
   apply (simp add: setObject_def split_def)
-  apply (rule hoare_seq_ext [OF _ hoare_gets_post])
+  apply (rule hoare_seq_ext [OF _ hoare_gets_sp])
   apply (clarsimp simp: valid_def in_monad)
   apply (frule updateObject_type)
   apply (drule R)
diff --git a/proof/refine/ARM_HYP/KHeap_R.thy b/proof/refine/ARM_HYP/KHeap_R.thy
index dd9b8dd5d..2a05f30b0 100644
--- a/proof/refine/ARM_HYP/KHeap_R.thy
+++ b/proof/refine/ARM_HYP/KHeap_R.thy
@@ -254,7 +254,7 @@ lemma obj_at_setObject1:
    setObject p (v::'a::pspace_storable)
   \<lbrace> \<lambda>rv. obj_at' (\<lambda>x::'a::pspace_storable. True) t \<rbrace>"
   apply (simp add: setObject_def split_def)
-  apply (rule hoare_seq_ext [OF _ hoare_gets_post])
+  apply (rule hoare_seq_ext [OF _ hoare_gets_sp])
   apply (clarsimp simp: valid_def in_monad obj_at'_def
                         projectKOs lookupAround2_char1
                         project_inject
@@ -276,7 +276,7 @@ lemma obj_at_setObject2:
    setObject p (v::'a)
   \<lbrace> \<lambda>rv. obj_at' P t \<rbrace>"
   apply (simp add: setObject_def split_def)
-  apply (rule hoare_seq_ext [OF _ hoare_gets_post])
+  apply (rule hoare_seq_ext [OF _ hoare_gets_sp])
   apply (clarsimp simp: valid_def in_monad)
   apply (frule updateObject_type)
   apply (drule R)
diff --git a/proof/refine/RISCV64/KHeap_R.thy b/proof/refine/RISCV64/KHeap_R.thy
index 4574417ea..0ef817441 100644
--- a/proof/refine/RISCV64/KHeap_R.thy
+++ b/proof/refine/RISCV64/KHeap_R.thy
@@ -183,7 +183,7 @@ lemma obj_at_setObject1:
    setObject p (v::'a::pspace_storable)
   \<lbrace> \<lambda>rv. obj_at' (\<lambda>x::'a::pspace_storable. True) t \<rbrace>"
   apply (simp add: setObject_def split_def)
-  apply (rule hoare_seq_ext [OF _ hoare_gets_post])
+  apply (rule hoare_seq_ext [OF _ hoare_gets_sp])
   apply (clarsimp simp: valid_def in_monad obj_at'_def lookupAround2_char1 project_inject
                  dest!: R)
   apply (subgoal_tac "objBitsKO (injectKO v) = objBitsKO (injectKO obj)")
@@ -203,7 +203,7 @@ lemma obj_at_setObject2:
    setObject p (v::'a)
   \<lbrace> \<lambda>rv. obj_at' P t \<rbrace>"
   apply (simp add: setObject_def split_def)
-  apply (rule hoare_seq_ext [OF _ hoare_gets_post])
+  apply (rule hoare_seq_ext [OF _ hoare_gets_sp])
   apply (clarsimp simp: valid_def in_monad)
   apply (frule updateObject_type)
   apply (drule R)
diff --git a/proof/refine/X64/KHeap_R.thy b/proof/refine/X64/KHeap_R.thy
index 689169999..4fd7fb09b 100644
--- a/proof/refine/X64/KHeap_R.thy
+++ b/proof/refine/X64/KHeap_R.thy
@@ -188,7 +188,7 @@ lemma obj_at_setObject1:
    setObject p (v::'a::pspace_storable)
   \<lbrace> \<lambda>rv. obj_at' (\<lambda>x::'a::pspace_storable. True) t \<rbrace>"
   apply (simp add: setObject_def split_def)
-  apply (rule hoare_seq_ext [OF _ hoare_gets_post])
+  apply (rule hoare_seq_ext [OF _ hoare_gets_sp])
   apply (clarsimp simp: valid_def in_monad obj_at'_def
                         projectKOs lookupAround2_char1
                         project_inject
@@ -210,7 +210,7 @@ lemma obj_at_setObject2:
    setObject p (v::'a)
   \<lbrace> \<lambda>rv. obj_at' P t \<rbrace>"
   apply (simp add: setObject_def split_def)
-  apply (rule hoare_seq_ext [OF _ hoare_gets_post])
+  apply (rule hoare_seq_ext [OF _ hoare_gets_sp])
   apply (clarsimp simp: valid_def in_monad)
   apply (frule updateObject_type)
   apply (drule R)