--- 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' =>