diff --git a/Isabelle_DOF/thys/Isa_COL.thy b/Isabelle_DOF/thys/Isa_COL.thy
index a5e007f..522f991 100644
--- a/Isabelle_DOF/thys/Isa_COL.thy
+++ b/Isabelle_DOF/thys/Isa_COL.thy
@@ -804,14 +804,14 @@ fun upd_block f =
 fun upd_block_title f =
   upd_block (fn title => f title)
 
-val unenclose_end = unenclose
-val unenclose_string = unenclose o unenclose o unenclose_end
+val unenclose_string = unenclose o unenclose
 
 fun read_string s =
-  let val symbols = unenclose_end s |> Symbol_Pos.explode0
+  let val s' = DOF_core.markup2string s
+      val symbols = s' |> Symbol_Pos.explode0
   in if hd symbols |> fst |> equal Symbol.open_
      then Token.read_cartouche symbols |> Token.input_of
-     else unenclose_string s |> Syntax.read_input
+     else unenclose_string s' |> Syntax.read_input
   end
 
 val block_titleN = "title"
diff --git a/Isabelle_DOF/thys/Isa_DOF.thy b/Isabelle_DOF/thys/Isa_DOF.thy
index 409a67a..70a350c 100644
--- a/Isabelle_DOF/thys/Isa_DOF.thy
+++ b/Isabelle_DOF/thys/Isa_DOF.thy
@@ -2847,12 +2847,13 @@ fun pretty_docitem_antiquotation_generic cid_decl ctxt ({unchecked, define}, src
         val inline = Config.get ctxt Document_Antiquotation.thy_output_display
         val _ = check_and_mark ctxt cid_decl {strict_checking = not unchecked} 
                                              {inline = inline} pos str
+        val cid_decl' = DOF_core.output_name cid_decl
     in  
         (case (define,inline) of
-            (true,false) => XML.enclose("{\\isaDofDOTlabel[type={"^cid_decl^"}]   {")"}}" 
-           |(false,false)=> XML.enclose("{\\isaDofDOTref[type={"^cid_decl^"}]     {")"}}"
-           |(true,true)  => XML.enclose("{\\isaDofDOTmacroDef[type={"^cid_decl^"}]{")"}}" 
-           |(false,true) => XML.enclose("{\\isaDofDOTmacroExp[type={"^cid_decl^"}]{")"}}"
+            (true,false) => XML.enclose("{\\isaDofDOTlabel[type={"^cid_decl'^"}]   {")"}}" 
+           |(false,false)=> XML.enclose("{\\isaDofDOTref[type={"^cid_decl'^"}]     {")"}}"
+           |(true,true)  => XML.enclose("{\\isaDofDOTmacroDef[type={"^cid_decl'^"}]{")"}}" 
+           |(false,true) => XML.enclose("{\\isaDofDOTmacroExp[type={"^cid_decl'^"}]{")"}}"
         )
         (Latex.text (DOF_core.output_name str, pos))
     end