--- 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)