author | wenzelm |
Fri, 29 Oct 1999 12:49:50 +0200 | |
changeset 7973 | 0d801c6e4dc0 |
parent 7972 | b95d183ae476 |
child 7974 | 34245feb6e82 |
--- 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