1.1 --- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Wed Nov 03 20:19:24 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Wed Nov 03 22:26:53 2010 +0100
     1.3 @@ -52,6 +52,7 @@
     1.4    val pretty_serial_commas : string -> Pretty.T list -> Pretty.T list
     1.5    val parse_bool_option : bool -> string -> string -> bool option
     1.6    val parse_time_option : string -> string -> Time.time option
     1.7 +  val string_from_time : Time.time -> string
     1.8    val nat_subscript : int -> string
     1.9    val flip_polarity : polarity -> polarity
    1.10    val prop_T : typ
    1.11 @@ -237,6 +238,7 @@
    1.12  
    1.13  val parse_bool_option = Sledgehammer_Util.parse_bool_option
    1.14  val parse_time_option = Sledgehammer_Util.parse_time_option
    1.15 +val string_from_time = Sledgehammer_Util.string_from_time
    1.16  
    1.17  val i_subscript = implode o map (prefix "\<^isub>") o explode
    1.18  fun be_subscript s = "\<^bsub>" ^ s ^ "\<^esub>"