diff -r e654599b114e -r ad2f5da643b4 src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Sun Jan 25 00:42:22 2004 +0100
+++ b/src/Pure/Thy/latex.ML	Mon Jan 26 10:34:02 2004 +0100
@@ -69,7 +69,8 @@
   if size s = 1 then output_chr s
   else
     (case explode s of
-      "\\" :: "<" :: "^" :: cs => "\\isactrl" ^ 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");