# HG changeset patch
# User huffman
# Date 1257216593 28800
# Node ID d9a25a87da4a226c1531daa79857bc5f220a8543
# Parent  fc43fa403a695c785731dc994a5278a568be6ee7# Parent  daa526c9e5d20ef6e63e684cb042982d27c16c38
merge

diff -r fc43fa403a69 -r d9a25a87da4a src/HOL/Tools/Function/lexicographic_order.ML
--- a/src/HOL/Tools/Function/lexicographic_order.ML	Mon Nov 02 18:39:41 2009 -0800
+++ b/src/HOL/Tools/Function/lexicographic_order.ML	Mon Nov 02 18:49:53 2009 -0800
@@ -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)