From 3f66cb0005305adbd542f0b0aeba061aad28ff0f Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Fri, 1 Sep 2023 18:27:31 +0200 Subject: [PATCH] lib/Eisbach_Tools: morphism type changed in Isabelle2023 Signed-off-by: Gerwin Klein --- lib/Eisbach_Tools/Apply_Debug.thy | 6 +++--- lib/Eisbach_Tools/Apply_Trace.thy | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/lib/Eisbach_Tools/Apply_Debug.thy b/lib/Eisbach_Tools/Apply_Debug.thy index ac9104eea..3a13e03dc 100644 --- a/lib/Eisbach_Tools/Apply_Debug.thy +++ b/lib/Eisbach_Tools/Apply_Debug.thy @@ -484,14 +484,14 @@ fun maybe_bind st (_,[tok]) ctxt = val local_facts = Facts.dest_static true [(Proof_Context.facts_of target)] local_facts; - val _ = Token.assign (SOME (Token.Declaration (fn phi => - Data.put (SOME (phi,ctxt, {private_dyn_facts = private_dyns, local_facts = local_facts}))))) tok; + val _ = Token.assign (SOME (Token.Declaration (Morphism.entity (fn phi => + Data.put (SOME (phi,ctxt, {private_dyn_facts = private_dyns, local_facts = local_facts})))))) tok; in ctxt end else let val SOME (Token.Declaration decl) = Token.get_value tok; - val dummy_ctxt = decl Morphism.identity (Context.Proof ctxt); + val dummy_ctxt = Morphism.form decl (Context.Proof ctxt); val SOME (phi,static_ctxt,{private_dyn_facts, local_facts}) = Data.get dummy_ctxt; val old_facts = Proof_Context.facts_of static_ctxt; diff --git a/lib/Eisbach_Tools/Apply_Trace.thy b/lib/Eisbach_Tools/Apply_Trace.thy index dba9ed505..3e7a0943e 100644 --- a/lib/Eisbach_Tools/Apply_Trace.thy +++ b/lib/Eisbach_Tools/Apply_Trace.thy @@ -225,7 +225,7 @@ let val deps = case query of SOME (raw_query,pos) => let - val pos' = perhaps (try (Position.advance_offsets 1)) pos; + val pos' = perhaps (try (Position.shift_offsets {remove_id = false} 1)) pos; val q = Find_Theorems.read_query pos' raw_query; val results = Find_Theorems.find_theorems_cmd ctxt (SOME thm) (SOME 1000000000) false q |> snd