tuned signature;

--- a/src/Doc/Implementation/ML.thy	Sun Oct 18 20:43:56 2015 +0200
+++ b/src/Doc/Implementation/ML.thy	Sun Oct 18 20:48:24 2015 +0200
@@ -1306,7 +1306,7 @@
   \<^descr> Type @{ML_type "Symbol.sym"} is a concrete datatype that
   represents the different kinds of symbols explicitly, with
   constructors @{ML "Symbol.Char"}, @{ML "Symbol.UTF8"},
-  @{ML "Symbol.Sym"}, @{ML "Symbol.Ctrl"}, @{ML "Symbol.Raw"},
+  @{ML "Symbol.Sym"}, @{ML "Symbol.Control"}, @{ML "Symbol.Raw"},
   @{ML "Symbol.Malformed"}.
 
   \<^descr> @{ML "Symbol.decode"} converts the string representation of a

--- a/src/Pure/General/antiquote.ML	Sun Oct 18 20:43:56 2015 +0200
+++ b/src/Pure/General/antiquote.ML	Sun Oct 18 20:48:24 2015 +0200
@@ -94,7 +94,7 @@
   Scan.trace (Symbol_Pos.scan_cartouche err_prefix) >>
     (fn ((control, pos), (_, body)) =>
       let
-        val Symbol.Ctrl name = Symbol.decode control;
+        val Symbol.Control name = Symbol.decode control;
         val range = Symbol_Pos.range ((control, pos) :: body);
       in {name = (name, pos), range = range, body = body} end);
 

--- a/src/Pure/General/symbol.ML	Sun Oct 18 20:43:56 2015 +0200
+++ b/src/Pure/General/symbol.ML	Sun Oct 18 20:48:24 2015 +0200
@@ -40,7 +40,7 @@
   val decode_raw: symbol -> string
   val encode_raw: string -> string
   datatype sym =
-    Char of string | UTF8 of string | Sym of string | Ctrl of string | Raw of string |
+    Char of string | UTF8 of string | Sym of string | Control of string | Raw of string |
     Malformed of string | EOF
   val decode: symbol -> sym
   datatype kind = Letter | Digit | Quasi | Blank | Other
@@ -223,7 +223,7 @@
 (* symbol variants *)
 
 datatype sym =
-  Char of string | UTF8 of string | Sym of string | Ctrl of string | Raw of string |
+  Char of string | UTF8 of string | Sym of string | Control of string | Raw of string |
   Malformed of string | EOF;
 
 fun decode s =
@@ -232,7 +232,7 @@
   else if is_utf8 s then UTF8 s
   else if is_raw s then Raw (decode_raw s)
   else if is_malformed s then Malformed s
-  else if is_control s then Ctrl (String.substring (s, 3, size s - 4))
+  else if is_control s then Control (String.substring (s, 3, size s - 4))
   else Sym (String.substring (s, 2, size s - 3));
 
 

--- a/src/Pure/Thy/latex.ML	Sun Oct 18 20:43:56 2015 +0200
+++ b/src/Pure/Thy/latex.ML	Sun Oct 18 20:48:24 2015 +0200
@@ -94,14 +94,14 @@
     Symbol.Char s => output_chr s
   | Symbol.UTF8 s => s
   | Symbol.Sym s => if known_sym s then enclose "{\\isasym" "}" s else output_chrs sym
-  | Symbol.Ctrl s => if known_ctrl s then enclose "\\isactrl" " " s else output_chrs sym
+  | Symbol.Control s => if known_ctrl s then enclose "\\isactrl" " " s else output_chrs sym
   | Symbol.Raw s => s
   | Symbol.Malformed s => error (Symbol.malformed_msg s)
   | Symbol.EOF => error "Bad EOF symbol");
 
 fun output_ctrl_sym sym =
   (case Symbol.decode sym of
-    Symbol.Ctrl s => enclose "\\isactrl" " " s
+    Symbol.Control s => enclose "\\isactrl" " " s
   | _ => sym);
 
 in