# HG changeset patch # User blanchet # Date 1358279490 -3600 # Node ID 3d2d62d293029e598fef6fd73dece90f837f5890 # Parent 8226f9a1273abf60f6669205305f6e9ffe4961bc tuned whitespace diff -r 8226f9a1273a -r 3d2d62d29302 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Jan 15 20:22:01 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Jan 15 20:51:30 2013 +0100 @@ -217,8 +217,7 @@ provers else provers - |> (if blocking then Par_List.map else map) - (launch problem #> fst) + |> (if blocking then Par_List.map else map) (launch problem #> fst) |> max_outcome_code |> rpair state end fun get_facts label is_appropriate_prop provers =