From 0f99a7530060ab00e360d076a9846ebc39df3bfd Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Sat, 16 Sep 2023 11:11:53 +0200 Subject: [PATCH] autocorres: update to Isabelle2023 Signed-off-by: Gerwin Klein --- tools/autocorres/TypHeapSimple.thy | 4 ++-- tools/autocorres/utils.ML | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/tools/autocorres/TypHeapSimple.thy b/tools/autocorres/TypHeapSimple.thy index 074ec1932c..d5e303c10a 100644 --- a/tools/autocorres/TypHeapSimple.thy +++ b/tools/autocorres/TypHeapSimple.thy @@ -512,7 +512,7 @@ lemma simple_lift_field_update': and xf_xfu: "fg_cons xf xfu" and cl: "simple_lift hp ptr = Some z" shows "(simple_lift (hrs_mem_update (heap_update (Ptr &(ptr\f)) val) hp)) = - simple_lift hp(ptr \ xfu val z)" + (simple_lift hp)(ptr \ xfu val z)" (is "?LHS = ?RHS") proof (rule ext) fix p @@ -581,7 +581,7 @@ lemma simple_lift_field_update: and xf_xfu: "fg_cons xf (xfu o (\x _. x))" and cl: "simple_lift hp ptr = Some z" shows "(simple_lift (hrs_mem_update (heap_update (Ptr &(ptr\f)) val) hp)) = - simple_lift hp(ptr \ xfu (\_. val) z)" + (simple_lift hp)(ptr \ xfu (\_. val) z)" (is "?LHS = ?RHS") apply (insert fl [unfolded field_ti_def]) apply (clarsimp split: option.splits) diff --git a/tools/autocorres/utils.ML b/tools/autocorres/utils.ML index 6059cb8055..cdb45d5394 100644 --- a/tools/autocorres/utils.ML +++ b/tools/autocorres/utils.ML @@ -459,7 +459,7 @@ fun term_fold_map_top f x = *) fun simp_map f = Context.map_proof ( - Local_Theory.declaration {syntax = false, pervasive = false} ( + Local_Theory.declaration {syntax = false, pervasive = false, pos = @{here}} ( K (Simplifier.map_ss f))) |> Context.proof_map