changeset 36402 | 1b20805974c7 |
parent 36378 | f32c567dbcaa |
child 36478 | 1aba777a367f |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Mon Apr 26 21:18:20 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Mon Apr 26 21:20:43 2010 +0200 @@ -38,7 +38,6 @@ else aux (String.sub (s, 0) :: seen) (String.extract (s, 1, NONE)) in aux [] end - fun remove_all bef = replace_all bef "" val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now