diff --git a/proof/refine/AARCH64/ArchInvsLemmas_H.thy b/proof/refine/AARCH64/ArchInvsLemmas_H.thy
index f3fe591a7f..7e5fa1fdb8 100644
--- a/proof/refine/AARCH64/ArchInvsLemmas_H.thy
+++ b/proof/refine/AARCH64/ArchInvsLemmas_H.thy
@@ -455,6 +455,7 @@ lemma objBitsT_simps:
 (* interface lemma - exports only generic equations from objBitsT_simps *)
 lemmas gen_objBitsT_simps = objBitsT_simps(1-7)
 
+(* interface lemma *)
 lemma objBitsT_koTypeOf:
   "(objBitsT (koTypeOf ko)) = objBitsKO ko"
   apply (cases ko; simp add: objBits_simps objBitsT_simps)
diff --git a/proof/refine/AARCH64/InvariantUpdates_H.thy b/proof/refine/AARCH64/InvariantUpdates_H.thy
index 3d5ba30906..e701d84c22 100644
--- a/proof/refine/AARCH64/InvariantUpdates_H.thy
+++ b/proof/refine/AARCH64/InvariantUpdates_H.thy
@@ -8,7 +8,7 @@ theory InvariantUpdates_H
 imports ArchInvsLemmas_H
 begin
 
-(* generic consequences which require arch-specific proofs *)
+(* generic consequences which require arch-specific proofs from ArchInvsLemmas_H *)
 arch_requalify_facts
   cte_wp_atE'
   cte_wp_at_cteI'
@@ -17,8 +17,9 @@ arch_requalify_facts
   valid_arch_tcb_lift'
   tcb_at_cte_at'
   gen_objBitsT_simps
+  objBitsT_koTypeOf (* FIXME arch-split: consider declaring [simp] here rather than Schedule_R *)
 
-(* arch-specific typ_at_lifts in Arch *)
+(* arch-specific typ_at_lifts in Arch *) (* FIXME arch-split: currently unused *)
 lemmas gen_typ_at_lifts =
          typ_at_lift_tcb' typ_at_lift_ep' typ_at_lift_ntfn' typ_at_lift_cte' typ_at_lift_cte_at'
          typ_at_lift_valid_untyped' typ_at_lift_valid_cap' valid_bound_tcb_lift