src/Pure/thm.ML
changeset 8854 c2cd9e1b6142
parent 8831 b824c0c55613
child 9031 8f75b9ce2f06
--- 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*)