\<^raw...> does no longer print an additional space.
--- 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");