src/HOL/Tools/Nitpick/nitpick_util.ML

   val plural_s_for_list : 'a list -> string
   val serial_commas : string -> string list -> string list
   val pretty_serial_commas : string -> Pretty.T list -> Pretty.T list
   val parse_bool_option : bool -> string -> string -> bool option
   val parse_time_option : string -> string -> Time.time option
-  val string_from_time : Time.time -> string
+  val string_of_time : Time.time -> string
   val nat_subscript : int -> string
   val flip_polarity : polarity -> polarity
   val prop_T : typ
   val bool_T : typ
   val nat_T : typ

   | pretty_serial_commas conj (p :: ps) =
     p :: Pretty.str "," :: Pretty.brk 1 :: pretty_serial_commas conj ps
 
 val parse_bool_option = Sledgehammer_Util.parse_bool_option
 val parse_time_option = Sledgehammer_Util.parse_time_option
-val string_from_time = ATP_Util.string_from_time
+val string_of_time = ATP_Util.string_of_time
 
 val i_subscript = implode o map (prefix "\<^isub>") o Symbol.explode
 fun nat_subscript n =
   n |> signed_string_of_int |> print_mode_active Symbol.xsymbolsN ? i_subscript