--- a/src/Pure/Thy/latex.ML Tue Oct 10 23:43:47 2000 +0200
+++ b/src/Pure/Thy/latex.ML Tue Oct 10 23:44:44 2000 +0200
@@ -61,13 +61,13 @@
"|" => "{\\isacharbar}" |
"}" => "{\\isacharbraceright}" |
"~" => "{\\isachartilde}" |
- c => if Symbol.is_digit c then enclose "\\isadigit{" "}" c else c;
+ c => if Symbol.is_digit c then enclose "{\\isadigit{" "}}" c else c;
fun output_sym s =
if size s = 1 then output_chr s
else
(case explode s of
- cs as "\\" :: "<" :: "^" :: _ => implode (map output_chr cs)
+ "\\" :: "<" :: "^" :: cs => "\\isactrl" ^ implode (#1 (Library.split_last cs)) ^ " "
| "\\" :: "<" :: cs => "{\\isasym" ^ implode (#1 (Library.split_last cs)) ^ "}"
| _ => sys_error "output_sym");