# HG changeset patch
# User wenzelm
# Date 1331590614 -3600
# Node ID 9920f9a75b5125e39a801f3bf111b023766df3a0
# Parent  af4c1dd3963f8e19c10ca71d0e976155842745c6
Par_List.map is already smart;

diff -r af4c1dd3963f -r 9920f9a75b51 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Mon Mar 12 23:16:02 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Mon Mar 12 23:16:54 2012 +0100
@@ -268,12 +268,6 @@
   ctxt |> select_smt_solver name
        |> SMT_Config.solver_class_of |> SMT_Utils.string_of_class
 
-(* Makes backtraces more transparent and might well be more efficient as
-   well. *)
-fun smart_par_list_map _ [] = []
-  | smart_par_list_map f [x] = [f x]
-  | smart_par_list_map f xs = Par_List.map f xs
-
 fun dest_SMT_Weighted_Fact (SMT_Weighted_Fact p) = p
   | dest_SMT_Weighted_Fact _ = raise Fail "dest_SMT_Weighted_Fact"
 
@@ -330,7 +324,7 @@
                     provers
           else
             provers
-            |> (if blocking then smart_par_list_map else map)
+            |> (if blocking then Par_List.map else map)
                    (launch problem #> fst)
             |> max_outcome_code |> rpair state
         end
@@ -407,7 +401,7 @@
         launch_atps "Unit equational provers" (SOME is_unit_equality) ueq_atps
       fun launch_atps_and_smt_solvers () =
         [launch_full_atps, launch_smts, launch_ueq_atps]
-        |> smart_par_list_map (fn f => ignore (f (unknownN, state)))
+        |> Par_List.map (fn f => ignore (f (unknownN, state)))
         handle ERROR msg => (print ("Error: " ^ msg); error msg)
       fun maybe f (accum as (outcome_code, _)) =
         accum |> (mode = Normal orelse outcome_code <> someN) ? f