# HG changeset patch
# User wenzelm
# Date 1454421879 -3600
# Node ID 614d88f87cfe853cbe00341545ec4b9934b7cdf7
# Parent  f3736c02cb3f9cb0e1772653061f29aae4aeadc9
proper markup for formal text;

diff -r f3736c02cb3f -r 614d88f87cfe src/Pure/Thy/document_antiquotations.ML
--- a/src/Pure/Thy/document_antiquotations.ML	Mon Feb 01 16:58:24 2016 +0100
+++ b/src/Pure/Thy/document_antiquotations.ML	Tue Feb 02 15:04:39 2016 +0100
@@ -217,7 +217,9 @@
   Theory.setup
    (entity_antiquotation @{binding command} Outer_Syntax.check_command
      (enclose "\\isacommand{" "}" o Output.output) #>
-    entity_antiquotation @{binding method} Method.check_name Output.output #>
-    entity_antiquotation @{binding attribute} Attrib.check_name Output.output);
+    entity_antiquotation @{binding method} Method.check_name
+     (enclose "\\isa{" "}" o Output.output) #>
+    entity_antiquotation @{binding attribute} Attrib.check_name
+     (enclose "\\isa{" "}" o Output.output));
 
 end;