--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Jun 26 19:40:58 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Jun 26 20:32:31 2014 +0200
@@ -264,9 +264,10 @@
if outcome_code = someN then accum else launch problem prover)
provers
else
- provers
- |> (if blocking then Par_List.map else map) (launch problem #> fst)
- |> max_outcome_code |> rpair state
+ (learn chained;
+ provers
+ |> (if blocking then Par_List.map else map) (launch problem #> fst)
+ |> max_outcome_code |> rpair state)
end
in
(if blocking then launch_provers state