diff -r 31252c4d4923 -r 1b20805974c7 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- 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