# HG changeset patch
# User wenzelm
# Date 957985392 -7200
# Node ID c2cd9e1b6142d573d474e0c6719c93804a67cd71
# Parent  079f607dc3ddd5de00c39aba246d6e6c24396f0d
dest_mss: sort procs wrt. names;

diff -r 079f607dc3dd -r c2cd9e1b6142 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*)