diff --git a/proof/invariant-abstract/ARM_HYP/ArchDetSchedSchedule_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchDetSchedSchedule_AI.thy
index 2a062073b..72368f4d7 100644
--- a/proof/invariant-abstract/ARM_HYP/ArchDetSchedSchedule_AI.thy
+++ b/proof/invariant-abstract/ARM_HYP/ArchDetSchedSchedule_AI.thy
@@ -446,8 +446,8 @@ lemma vgic_maintenance_irq_valid_sched[wp]:
   unfolding vgic_maintenance_def
             get_gic_vcpu_ctrl_misr_def get_gic_vcpu_ctrl_eisr1_def get_gic_vcpu_ctrl_eisr0_def
   apply (wpsimp wp: handle_fault_valid_sched thread_get_wp'
-              simp: do_machine_op_bind valid_fault_def
-         | rule conjI | strengthen conj_imp_strg)+
+              simp: do_machine_op_bind valid_fault_def submonad_do_machine_op.gets
+         | intro conjI impI)+
   apply (clarsimp simp: st_tcb_at_def obj_at_def runnable_eq)
   done
 
diff --git a/proof/invariant-abstract/ARM_HYP/ArchInterrupt_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchInterrupt_AI.thy
index a7883af68..d023779ae 100644
--- a/proof/invariant-abstract/ARM_HYP/ArchInterrupt_AI.thy
+++ b/proof/invariant-abstract/ARM_HYP/ArchInterrupt_AI.thy
@@ -212,11 +212,11 @@ lemma vgic_maintenance_invs[wp]:
   "\<lbrace>invs\<rbrace> vgic_maintenance \<lbrace>\<lambda>_. invs\<rbrace>"
   unfolding vgic_maintenance_def get_gic_vcpu_ctrl_misr_def
             get_gic_vcpu_ctrl_eisr1_def get_gic_vcpu_ctrl_eisr0_def
-  apply (wpsimp simp: valid_fault_def do_machine_op_bind ct_in_state_def
+  apply (wpsimp simp: do_machine_op_bind submonad_do_machine_op.gets valid_fault_def
                   wp: thread_get_wp'
-         | strengthen conj_imp_strg)+
+         | intro conjI impI)+
   apply (fastforce intro!: st_tcb_ex_cap[where P=active]
-                     simp: st_tcb_at_def obj_at_def runnable_eq halted_eq)
+                     simp: st_tcb_at_def obj_at_def runnable_eq halted_eq)+
   done
 
 lemma handle_reserved_irq_invs[wp]: