From 331fcd07f0f816f914608cf38bdc68b8d3bfaf72 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Mon, 20 Nov 2023 16:57:01 +0100 Subject: [PATCH] Update invariants checking Make invariants checking compatible with namespaces and the new invariants implementation --- Isabelle_DOF/thys/Isa_DOF.thy | 14 +++++--------- 1 file changed, 5 insertions(+), 9 deletions(-) diff --git a/Isabelle_DOF/thys/Isa_DOF.thy b/Isabelle_DOF/thys/Isa_DOF.thy index 4d09564..d383f8d 100644 --- a/Isabelle_DOF/thys/Isa_DOF.thy +++ b/Isabelle_DOF/thys/Isa_DOF.thy @@ -1798,20 +1798,16 @@ fun check_invariants thy binding = val cids_invariants = get_all_invariants name thy val inv_and_apply_list = let fun mk_inv_and_apply cid_invs value thy = - let val (cid_long, invs) = cid_invs - val inv_def_typ = Term.type_of value + let val ctxt = Proof_Context.init_global thy + val (cid_long, invs) = cid_invs in invs |> map (fn (bind, _) => let val inv_name = Binding.name_of bind - |> Long_Name.qualify (Long_Name.base_name cid_long) + |> Long_Name.qualify cid_long val pos = Binding.pos_of bind - val inv_def = inv_name - |> Syntax.read_term_global thy - in case inv_def of - Const (s, Type (st, [_ (*ty*), ty'])) => - ((inv_name, pos), Const (s, Type (st,[inv_def_typ, ty'])) $ value) - | _ => ((inv_name, pos), inv_def $ value) end) + val inv_def = inv_name |> Syntax.parse_term ctxt + in ((inv_name, pos), Syntax.check_term ctxt (inv_def $ value)) end) end in cids_invariants |> map (fn cid_invs => mk_inv_and_apply cid_invs docitem_value thy) |> flat