From 0e7f3c4cdcb6e8687eeefad210c3e470b89f3964 Mon Sep 17 00:00:00 2001 From: bu Date: Wed, 3 Jul 2019 11:30:18 +0200 Subject: [PATCH] locals --- Isa_DOF.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Isa_DOF.thy b/Isa_DOF.thy index badfcf6b..29f4a712 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -1657,7 +1657,7 @@ fun check_and_mark ctxt cid_decl (str:{strict_checking: bool}) pos name = in () end else if DOF_core.is_declared_oid_global name thy then (if #strict_checking str - then warning("declared but undefined document reference:"^name)(* HACK bu 29/6.19 *) + then warning("declared but undefined document reference:"^name)(* HACK bu 29/6.19 *) else ()) else error("undefined document reference:"^name) end