--- a/src/Pure/General/symbol.ML Mon Jun 05 23:55:58 2017 +0200
+++ b/src/Pure/General/symbol.ML Tue Jun 06 13:13:25 2017 +0200
@@ -64,7 +64,6 @@
val bump_init: string -> string
val bump_string: string -> string
val length: symbol list -> int
- val xsymbolsN: string
val output: string -> Output.output * int
end;
@@ -466,11 +465,6 @@
fun sym_length ss = fold (fn s => fn n => sym_len s + n) ss 0;
-
-(* print mode *)
-
-val xsymbolsN = "xsymbols";
-
fun output s = (s, sym_length (Symbol.explode s));