diff --git a/proof/refine/AARCH64/ArchInvsDefs_H.thy b/proof/refine/AARCH64/ArchInvsDefs_H.thy
index 0006854927..8923dfff59 100644
--- a/proof/refine/AARCH64/ArchInvsDefs_H.thy
+++ b/proof/refine/AARCH64/ArchInvsDefs_H.thy
@@ -6,8 +6,8 @@
  *)
 
 (* This theory contains the arch-dependent part of invariant definitions.
-   Due to the large amount of definitins, we opt for a Pre file rather than fixing constants in
-   locales. *)
+   Due to the large amount of definitions, we place it before Invariants_H rather than fixing
+   constants in locales. *)
 
 theory ArchInvsDefs_H
 imports
@@ -33,7 +33,6 @@ requalify_facts (aliasing)
   Retype_H.createObject_def Retype_H.capUntypedPtr_def Retype_H.capUntypedSize_def
   Retype_H.performInvocation_def Retype_H.decodeInvocation_def
 end
-
 end
 
 context Arch begin arch_global_naming
diff --git a/proof/refine/Invariants_H.thy b/proof/refine/Invariants_H.thy
index 74cad3a718..bd93854d63 100644
--- a/proof/refine/Invariants_H.thy
+++ b/proof/refine/Invariants_H.thy
@@ -174,7 +174,6 @@ primrec live0' :: "Structures_H.kernel_object \<Rightarrow> bool" where
 
 (* hyp_refs *)
 
-(* FIXME arch-split: do we want to expose this, or put it in Arch? *)
 definition hyp_refs_of' :: "kernel_object \<Rightarrow> (obj_ref \<times> reftype) set" where
   "hyp_refs_of' x \<equiv> case x of
      (KOTCB tcb)           \<Rightarrow> tcb_hyp_refs' (tcbArch tcb)