src/Pure/General/symbol.ML
changeset 66020 a31760eee09d
parent 64275 ac2abc987cf9
child 67373 17f9fa98abab
--- 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));