# HG changeset patch
# User wenzelm
# Date 941194190 -7200
# Node ID 0d801c6e4dc0caaa4fe7c9c1d2972e1238838fd2
# Parent  b95d183ae476859dbad1777cef4043b139919bd7
\isasymbol renamed to \isasym;

diff -r b95d183ae476 -r 0d801c6e4dc0 src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Fri Oct 29 12:48:50 1999 +0200
+++ b/src/Pure/Thy/latex.ML	Fri Oct 29 12:49:50 1999 +0200
@@ -41,7 +41,7 @@
   else
     (case explode s of
       cs as "\\" :: "<" :: "^" :: _ => implode (map output_chr cs)
-    | "\\" :: "<" :: cs => "{\\isasymbol" ^ implode (#1 (Library.split_last cs)) ^ "}"
+    | "\\" :: "<" :: cs => "{\\isasym" ^ implode (#1 (Library.split_last cs)) ^ "}"
     | _ => sys_error "output_sym");
 
 in