From 96ec3d4372cf8828b5d756cf06c65d13014de75a Mon Sep 17 00:00:00 2001
From: Gerwin Klein <gerwin.klein@proofcraft.systems>
Date: Fri, 14 Jan 2022 09:58:26 +1100
Subject: [PATCH] isabelle2021-1: DSpecProofs

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
---
 proof/capDL-api/Retype_DP.thy | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/proof/capDL-api/Retype_DP.thy b/proof/capDL-api/Retype_DP.thy
index f2dbf47a9..485d0eba3 100644
--- a/proof/capDL-api/Retype_DP.thy
+++ b/proof/capDL-api/Retype_DP.thy
@@ -463,10 +463,10 @@ lemma invoke_untyped_one_has_children:
         apply wp
        apply simp
       apply (clarsimp simp:neq_Nil_conv)
-        apply auto[1]
+        apply (cases slot, fastforce)
        apply wp+
      apply (rule hoare_strengthen_post[OF generate_object_ids_rv])
-     apply (clarsimp simp:zip_is_empty)
+     apply clarsimp
     apply (wp unlessE_wp hoare_drop_imps | simp)+
   done