dest_mss: sort procs wrt. names;
authorwenzelm
Wed May 10 21:03:12 2000 +0200 (2000-05-10)
changeset 8854c2cd9e1b6142
parent 8853 079f607dc3dd
child 8855 ef4848bb0696
dest_mss: sort procs wrt. names;
src/Pure/thm.ML
     1.1 --- a/src/Pure/thm.ML	Wed May 10 16:43:39 2000 +0200
     1.2 +++ b/src/Pure/thm.ML	Wed May 10 21:03:12 2000 +0200
     1.3 @@ -1634,7 +1634,8 @@
     1.4     procs =
     1.5       map (fn (_, {name, lhs, id, ...}) => ((name, lhs), id)) (Net.dest procs)
     1.6       |> partition_eq eq_snd
     1.7 -     |> map (fn ps => (#1 (#1 (hd ps)), map (#2 o #1) ps))};
     1.8 +     |> map (fn ps => (#1 (#1 (hd ps)), map (#2 o #1) ps))
     1.9 +     |> Library.sort_wrt #1};
    1.10  
    1.11  
    1.12  (* merge_mss *)		(*NOTE: ignores mk_rews and termless of 2nd mss*)