merge
authorhuffman
Mon Nov 02 18:49:53 2009 -0800 (2009-11-02)
changeset 33402d9a25a87da4a
parent 33401 fc43fa403a69
parent 33398 daa526c9e5d2
child 33403 a9b6497391b0
child 33420 17b7095ad463
child 33425 7e4f3c66190d
merge
     1.1 --- a/src/HOL/Tools/Function/lexicographic_order.ML	Mon Nov 02 18:39:41 2009 -0800
     1.2 +++ b/src/HOL/Tools/Function/lexicographic_order.ML	Mon Nov 02 18:49:53 2009 -0800
     1.3 @@ -197,7 +197,7 @@
     1.4        val measure_funs = MeasureFunctions.get_measure_functions ctxt domT (* 1: generate measures *)
     1.5  
     1.6        (* 2: create table *)
     1.7 -      val table = map (fn t => map (mk_cell thy solve_tac (dest_term t)) measure_funs) tl
     1.8 +      val table = Par_List.map (fn t => Par_List.map (mk_cell thy solve_tac (dest_term t)) measure_funs) tl
     1.9      in
    1.10        case search_table table of
    1.11          NONE => if quiet then no_tac st else error (no_order_msg ctxt table tl measure_funs)