src/Pure/Thy/document_antiquotations.ML

     (fn ctxt => fn (url, pos) =>
       let val _ = Context_Position.reports ctxt [(pos, Markup.language_path), (pos, Markup.url url)]
       in Latex.enclose_block "\\url{" "}" [Latex.string url] end));
 
 
-(* doc entries *)
-
-val _ = Theory.setup
-  (Thy_Output.antiquotation_pretty \<^binding>\<open>doc\<close> (Scan.lift (Parse.position Parse.embedded))
-    (fn ctxt => fn (name, pos) =>
-      let val _ = Context_Position.report ctxt pos (Markup.doc name)
-      in [Pretty.str name] end));
-
-
 (* formal entities *)
 
 local
 
 fun entity_antiquotation name check bg en =