# HG changeset patch # User schirmer # Date 1075193054 -3600 # Node ID fc62df0bf3532dfdec2a0435ba23a73ca9394423 # Parent 2c116016f95d2465859877c6b0d8146855ea37e2 \<^raw...> does no longer print an additional space. diff -r 2c116016f95d -r fc62df0bf353 src/Pure/Thy/latex.ML --- a/src/Pure/Thy/latex.ML Tue Jan 27 08:15:10 2004 +0100 +++ b/src/Pure/Thy/latex.ML Tue Jan 27 09:44:14 2004 +0100 @@ -69,7 +69,7 @@ if size s = 1 then output_chr s else (case explode s of - "\\" :: "<" :: "^" :: "r"::"a"::"w":: cs => implode (#1 (Library.split_last cs)) ^ " " + "\\" :: "<" :: "^" :: "r"::"a"::"w":: cs => implode (#1 (Library.split_last cs)) | "\\" :: "<" :: "^" :: cs => "\\isactrl" ^ implode (#1 (Library.split_last cs)) ^ " " | "\\" :: "<" :: cs => "{\\isasym" ^ implode (#1 (Library.split_last cs)) ^ "}" | _ => sys_error "output_sym");