# HG changeset patch
# User blanchet
# Date 1406902053 -7200
# Node ID 92fe49c7ab3bcf7f1cef52dd832674abcd5659ae
# Parent  e081db351356c969e87be08840d3509594ccd899
peek instead of joining -- is perhaps less risky

diff -r e081db351356 -r 92fe49c7ab3b src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- 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' =>