peek instead of joining -- is perhaps less risky

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Aug 01 16:07:33 2014 +0200
@@ -101,7 +101,10 @@
           else (false, false)
       in
         if anonymous then
-          app_body (if enter_class then map_inclass_name else map_name) (Future.join body) accum
+          (case Future.peek body of
+            SOME (Exn.Res the_body) =>
+            app_body (if enter_class then map_inclass_name else map_name) the_body accum
+          | NONE => accum)
         else
           (case map_name name of
             SOME name' =>