# HG changeset patch
# User krauss
# Date 1257199566 -3600
# Node ID daa526c9e5d20ef6e63e684cb042982d27c16c38
# Parent  609389f3ea1e427c1a477510fcd1d98185ca76d5
lexicographic order: run local descent proofs in parallel

diff -r 609389f3ea1e -r daa526c9e5d2 src/HOL/Tools/Function/lexicographic_order.ML
--- a/src/HOL/Tools/Function/lexicographic_order.ML	Mon Nov 02 13:43:50 2009 -0800
+++ b/src/HOL/Tools/Function/lexicographic_order.ML	Mon Nov 02 23:06:06 2009 +0100
@@ -197,7 +197,7 @@
       val measure_funs = MeasureFunctions.get_measure_functions ctxt domT (* 1: generate measures *)
 
       (* 2: create table *)
-      val table = map (fn t => map (mk_cell thy solve_tac (dest_term t)) measure_funs) tl
+      val table = Par_List.map (fn t => Par_List.map (mk_cell thy solve_tac (dest_term t)) measure_funs) tl
     in
       case search_table table of
         NONE => if quiet then no_tac st else error (no_order_msg ctxt table tl measure_funs)