--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Tue Jul 27 17:32:55 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Tue Jul 27 17:43:11 2010 +0200
@@ -8,7 +8,6 @@
sig
val plural_s : int -> string
val serial_commas : string -> string list -> string list
- val timestamp : unit -> string
val strip_spaces : string -> string
val parse_bool_option : bool -> string -> string -> bool option
val parse_time_option : string -> string -> Time.time option
@@ -32,8 +31,6 @@
| serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
| serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
-val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now
-
fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
fun strip_spaces_in_list [] = ""