From e78a11487985bd4c7740ade884fe94df38c4c96e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Fri, 24 Nov 2023 18:12:50 +0100 Subject: [PATCH] Fix typo --- Isabelle_DOF/ontologies/scholarly_paper/scholarly_paper.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Isabelle_DOF/ontologies/scholarly_paper/scholarly_paper.thy b/Isabelle_DOF/ontologies/scholarly_paper/scholarly_paper.thy index c62d28b..5b55fc0 100644 --- a/Isabelle_DOF/ontologies/scholarly_paper/scholarly_paper.thy +++ b/Isabelle_DOF/ontologies/scholarly_paper/scholarly_paper.thy @@ -629,7 +629,7 @@ fun check ctxt cidS mon_id pos_opt = fun get_level_raw oid = ISA_core.compute_attr_access ctxt "level" oid NONE @{here}; fun get_level oid = dest_option (snd o HOLogic.dest_number) (get_level_raw (oid)); fun check_level_hd a = case (get_level (snd a)) of - NONE => error("Invariant violation: leading section" ^ snd a ^ + NONE => error("Invariant violation: leading section " ^ snd a ^ " must have lowest level") | SOME X => X fun check_group_elem level_hd a = case (get_level (snd a)) of