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