src/Pure/General/symbol.ML

   val kind: symbol -> kind
   val is_letter: symbol -> bool
   val is_digit: symbol -> bool
   val is_quasi: symbol -> bool
   val is_blank: symbol -> bool
-  val is_block_ctrl: symbol -> bool
-  val has_block_ctrl: symbol list -> bool
+  val is_control_block: symbol -> bool
+  val has_control_block: symbol list -> bool
   val is_quasi_letter: symbol -> bool
   val is_letdig: symbol -> bool
   val beginning: int -> symbol list -> string
   val esc: symbol -> string
   val escape: string -> string

 fun is_letter s = kind s = Letter;
 fun is_digit s = kind s = Digit;
 fun is_quasi s = kind s = Quasi;
 fun is_blank s = kind s = Blank;
 
-val is_block_ctrl = member (op =) ["\<^bsub>", "\<^esub>", "\<^bsup>", "\<^esup>"];
-val has_block_ctrl = exists is_block_ctrl;
+val is_control_block = member (op =) ["\<^bsub>", "\<^esub>", "\<^bsup>", "\<^esup>"];
+val has_control_block = exists is_control_block;
 
 fun is_quasi_letter s = let val k = kind s in k = Letter orelse k = Quasi end;
 fun is_letdig s = let val k = kind s in k = Letter orelse k = Digit orelse k = Quasi end;