# HG changeset patch
# User wenzelm
# Date 1086433651 -7200
# Node ID 23c73484312f474d170bbacbc97e7240e5925e0e
# Parent  7efc14398e82130f5eab6766205e59afb8a16e52
Symbol.decode;

diff -r 7efc14398e82 -r 23c73484312f src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Sat Jun 05 13:07:19 2004 +0200
+++ b/src/Pure/Thy/latex.ML	Sat Jun 05 13:07:31 2004 +0200
@@ -65,14 +65,12 @@
   "~" => "{\\isachartilde}" |
   c => if Symbol.is_digit c then enclose "{\\isadigit{" "}}" c else c;
 
-fun output_sym s =
-  if Symbol.is_char s then output_chr s
-  else if Symbol.is_raw s then Symbol.decode_raw s
-  else if String.isPrefix "\\<^" s then
-    enclose "\\isactrl" " " (String.substring (s, 3, size s - 4))
-  else if String.isPrefix "\\<" s then
-    enclose "{\\isasym" "}" (String.substring (s, 2, size s - 3))
-  else sys_error "output_sym";
+fun output_sym sym =
+  (case Symbol.decode sym of
+    Symbol.Char s => output_chr s
+  | Symbol.Sym s => enclose "{\\isasym" "}" s
+  | Symbol.Ctrl s => enclose "\\isactrl" " " s
+  | Symbol.Raw s => s);
 
 in