diff -r f072119afa4e -r 1da4ce092c0b src/Pure/library.ML
--- a/src/Pure/library.ML	Mon Apr 11 12:18:27 2005 +0200
+++ b/src/Pure/library.ML	Mon Apr 11 12:34:34 2005 +0200
@@ -128,6 +128,7 @@
   val radixstring: int * string * int -> string
   val string_of_int: int -> string
   val string_of_indexname: string * int -> string
+    (* CB: note alternative Syntax.string_of_vname has nicer syntax *)
   val read_radixint: int * string list -> int * string list
   val read_int: string list -> int * string list
   val oct_char: string -> string