src/Pure/Thy/latex.ML
changeset 7973 0d801c6e4dc0
parent 7900 e62973fccc97
child 8117 0a6173c9b2d0
--- 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