1.1 --- a/src/Pure/Thy/latex.ML	Tue Oct 10 23:43:47 2000 +0200
     1.2 +++ b/src/Pure/Thy/latex.ML	Tue Oct 10 23:44:44 2000 +0200
     1.3 @@ -61,13 +61,13 @@
     1.4    "|" => "{\\isacharbar}" |
     1.5    "}" => "{\\isacharbraceright}" |
     1.6    "~" => "{\\isachartilde}" |
     1.7 -  c => if Symbol.is_digit c then enclose "\\isadigit{" "}" c else c;
     1.8 +  c => if Symbol.is_digit c then enclose "{\\isadigit{" "}}" c else c;
     1.9  
    1.10  fun output_sym s =
    1.11    if size s = 1 then output_chr s
    1.12    else
    1.13      (case explode s of
    1.14 -      cs as "\\" :: "<" :: "^" :: _ => implode (map output_chr cs)
    1.15 +      "\\" :: "<" :: "^" :: cs => "\\isactrl" ^ implode (#1 (Library.split_last cs)) ^ " "
    1.16      | "\\" :: "<" :: cs => "{\\isasym" ^ implode (#1 (Library.split_last cs)) ^ "}"
    1.17      | _ => sys_error "output_sym");
    1.18