diff --git a/proof/crefine/ARM_HYP/Retype_C.thy b/proof/crefine/ARM_HYP/Retype_C.thy
index cacb24c27d9..798b5cf3f55 100644
--- a/proof/crefine/ARM_HYP/Retype_C.thy
+++ b/proof/crefine/ARM_HYP/Retype_C.thy
@@ -2785,6 +2785,9 @@ lemma hoarep_Cond_UNIV:
   apply simp
   done
 
+(* always unfold StrictC'_mode_object_defs together with api_object_defs *)
+lemmas api_object_defs = api_object_defs StrictC'_mode_object_defs
+
 lemma object_type_from_H_toAPIType_simps:
   "(object_type_from_H tp = scast seL4_UntypedObject) = (toAPIType tp = Some ArchTypes_H.apiobject_type.Untyped)"
   "(object_type_from_H tp = scast seL4_TCBObject) = (toAPIType tp = Some ArchTypes_H.apiobject_type.TCBObject)"