diff --git a/Isabelle_DOF/latex/styles/DOF-core.sty b/Isabelle_DOF/latex/styles/DOF-core.sty
index 65d04f0c..fc0c2dd3 100644
--- a/Isabelle_DOF/latex/styles/DOF-core.sty
+++ b/Isabelle_DOF/latex/styles/DOF-core.sty
@@ -155,10 +155,14 @@
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % begin: label and ref
-\newisadof{label}[label=,type=][1]{\label{#1}}
-\newisadof{ref}[label=,type=][1]{\autoref{#1}}
-\newisadof{macroDef}[label=,type=][1]{MMM \label{#1}}        %% place_holder
-\newisadof{macroExp}[label=,type=][1]{MMM \autoref{#1}}   %% place_holder
+\newkeycommand\iisaDoflabel[label=,type=][1]{\label{#1}}
+\def\isaDoflabel{\iisaDoflabel}
+\newkeycommand\iisaDofref[label=,type=][1]{\autoref{#1}}
+\def\isaDofref{\iisaDofref}
+\newkeycommand\iisaDofmacroDef[label=,type=][1]{MMM \label{#1}}        %% place_holder
+\def\isaDofmacroDef{\iisaDofmacroDef}
+\newkeycommand\iisaDofmacroExp[label=,type=][1]{MMM \autoref{#1}}   %% place_holder
+\def\isaDofmacroExp{\iisaDofmacroExp}
 % end: label and ref
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
diff --git a/Isabelle_DOF/thys/Isa_DOF.thy b/Isabelle_DOF/thys/Isa_DOF.thy
index 21f75528..68a60589 100644
--- a/Isabelle_DOF/thys/Isa_DOF.thy
+++ b/Isabelle_DOF/thys/Isa_DOF.thy
@@ -2824,10 +2824,10 @@ fun pretty_docitem_antiquotation_generic cid_decl ctxt ({unchecked, define}, src
                                              {inline = inline} pos str
     in  
         (case (define,inline) of
-            (true,false) => XML.enclose("\\csname isaDof.label\\endcsname[type={"^cid_decl^"}]   {")"}" 
-           |(false,false)=> XML.enclose("\\csname isaDof.ref\\endcsname[type={"^cid_decl^"}]     {")"}"
-           |(true,true)  => XML.enclose("\\csname isaDof.macroDef\\endcsname[type={"^cid_decl^"}]{")"}" 
-           |(false,true) => XML.enclose("\\csname isaDof.macroExp\\endcsname[type={"^cid_decl^"}]{")"}"
+            (true,false) => XML.enclose("{\\isaDoflabel[type={"^cid_decl^"}]   {")"}}" 
+           |(false,false)=> XML.enclose("{\\isaDofref[type={"^cid_decl^"}]     {")"}}"
+           |(true,true)  => XML.enclose("{\\isaDofmacroDef[type={"^cid_decl^"}]{")"}}" 
+           |(false,true) => XML.enclose("{\\isaDofmacroExp[type={"^cid_decl^"}]{")"}}"
         )
         (Latex.text (str, pos))
     end