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