From 15993c653601622ffedb8935f86beb5175e15907 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Tue, 2 Jul 2019 05:30:24 +0100 Subject: [PATCH] Bug fix: fixed label/ref generation. --- Isa_DOF.thy | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Isa_DOF.thy b/Isa_DOF.thy index 6fb4d86b..d219ae31 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -1688,8 +1688,8 @@ fun pretty_docitem_antiquotation_generic cid_decl ctxt ({unchecked = x, define = val _ = check_and_mark ctxt cid_decl ({strict_checking = not x}) pos str in - (if y then Latex.enclose_block ("\\csname isadof.label[type={"^cid_decl^"}]{") "}\\endcsname" - else Latex.enclose_block ("\\csname isadof.ref[type={"^cid_decl^"}]{") "}\\endcsname") + (if y then Latex.enclose_block ("\\csname isaDof.label\\endcsname[type={"^cid_decl^"}]{") "}" + else Latex.enclose_block ("\\csname isaDof.ref\\endcsname[type={"^cid_decl^"}]{") "}") [Latex.text (Input.source_content src)] end