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