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 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 = Sledgehammer_Util.string_from_time
 
 val i_subscript = implode o map (prefix "\<^isub>") o explode
 fun be_subscript s = "\<^bsub>" ^ s ^ "\<^esub>"
 fun nat_subscript n =
   let val s = signed_string_of_int n in