diff --git a/proof/crefine/X64/Arch_C.thy b/proof/crefine/X64/Arch_C.thy
index a1ea859c37..ad07f5ffad 100644
--- a/proof/crefine/X64/Arch_C.thy
+++ b/proof/crefine/X64/Arch_C.thy
@@ -1468,21 +1468,6 @@ lemma obj_at_pte_aligned:
                   elim!: is_aligned_weaken)
   done
 
-(* FIXME x64: dont know what these are for yet *)
-lemma addrFromPPtr_mask_5:
-  "addrFromPPtr ptr && mask (5::nat) = ptr && mask (5::nat)"
-  apply (simp add:addrFromPPtr_def X64.pptrBase_def)
-  apply word_bitwise
-  apply (simp add:mask_def)
-  done
-
-lemma addrFromPPtr_mask_6:
-  "addrFromPPtr ptr && mask (6::nat) = ptr && mask (6::nat)"
-  apply (simp add:addrFromPPtr_def X64.pptrBase_def)
-  apply word_bitwise
-  apply (simp add:mask_def)
-  done
-
 lemma cpde_relation_invalid:
  "cpde_relation pdea pde \<Longrightarrow> (pde_get_tag pde = scast pde_pde_pt \<and> pde_pde_pt_CL.present_CL (pde_pde_pt_lift pde) = 0) = isInvalidPDE pdea"
   apply (simp add: cpde_relation_def Let_def)