src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
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