diff -r 0b691782d6e5 -r 7d4a088dbc0e src/Pure/General/symbol_pos.ML
--- a/src/Pure/General/symbol_pos.ML	Sat Jan 13 21:41:36 2018 +0100
+++ b/src/Pure/General/symbol_pos.ML	Sun Jan 14 14:11:02 2018 +0100
@@ -34,9 +34,6 @@
   val scan_cartouche: string -> T list -> T list * T list
   val scan_cartouche_content: string -> T list -> T list * T list
   val recover_cartouche: T list -> T list * T list
-  val scan_blanks: T list -> T list * T list
-  val scan_cancel_cartouche: string -> T list -> T list * T list
-  val scan_comment_cartouche: string -> T list -> T list * T list
   val scan_comment: string -> T list -> T list * T list
   val scan_comment_body: string -> T list -> T list * T list
   val recover_comment: T list -> T list * T list
@@ -219,19 +216,6 @@
 val recover_cartouche = Scan.pass (SOME 0) scan_cartouche_depth;
 
 
-(* operator with cartouche argument *)
-
-val scan_blanks = Scan.many (Symbol.is_blank o symbol);
-
-fun scan_operator_cartouche blanks operator_symbol err_prefix =
-  (if blanks then $$$ operator_symbol @@@ scan_blanks else $$$ operator_symbol) @@@
-    !!! (fn () => err_prefix ^ "cartouche expected after " ^ quote operator_symbol)
-      (scan_cartouche err_prefix);
-
-val scan_cancel_cartouche = scan_operator_cartouche false Symbol.cancel;
-val scan_comment_cartouche = scan_operator_cartouche true Symbol.comment;
-
-
 (* ML-style comments *)
 
 local