output_basic: handle AltString token;

--- a/src/Pure/Thy/latex.ML	Sun Aug 28 16:04:52 2005 +0200
+++ b/src/Pure/Thy/latex.ML	Sun Aug 28 16:04:53 2005 +0200
@@ -104,7 +104,10 @@
       "\\isacommand{" ^ output_syms s ^ "}"
     else if T.is_kind T.Keyword tok andalso Syntax.is_ascii_identifier s then
       "\\isakeyword{" ^ output_syms s ^ "}"
-    else if T.is_kind T.String tok then output_syms (Library.quote s)
+    else if T.is_kind T.String tok then
+      enclose "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" (output_syms s)
+    else if T.is_kind T.AltString tok then
+      enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
     else if T.is_kind T.Verbatim tok then output_syms (enclose "{*" "*}" s)
     else output_syms s
   end;