# HG changeset patch
# User wenzelm
# Date 1697975812 -7200
# Node ID a6b3dfab6fc2f7a7bf102dd4b220e862560e52ec
# Parent  1829ba610c36f430b2312fdaff2a63d4efc51d3d
tuned;

diff -r 1829ba610c36 -r a6b3dfab6fc2 src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Sun Oct 22 12:18:23 2023 +0200
+++ b/src/Pure/raw_simplifier.ML	Sun Oct 22 13:56:52 2023 +0200
@@ -217,11 +217,9 @@
     proc: proc Morphism.entity,
     id: stamp * thm list};
 
-fun eq_simproc_id ((s1: stamp, ths1: thm list), (s2, ths2)) =
+fun eq_simproc0 (Simproc0 {id = (s1, ths1), ...}, Simproc0 {id = (s2, ths2), ...}) =
   s1 = s2 andalso eq_list Thm.eq_thm_prop (ths1, ths2);
 
-fun eq_simproc0 (Simproc0 a, Simproc0 b) = eq_simproc_id (#id a, #id b);
-
 
 (* solvers *)
 
@@ -293,9 +291,8 @@
  {simps = Net.entries rules
     |> map (fn {name, thm, ...} => (name, thm)),
   procs = Net.entries procs
-    |> map (fn Simproc0 {name, lhs, id, ...} => ((name, lhs), id))
-    |> partition_eq (eq_snd eq_simproc_id)
-    |> map (fn ps => (fst (fst (hd ps)), map (snd o fst) ps)),
+    |> partition_eq eq_simproc0
+    |> map (fn ps as Simproc0 {name, ...} :: _ => (name, map (fn Simproc0 {lhs, ...} => lhs) ps)),
   congs = congs |> fst |> Congtab.dest,
   weak_congs = congs |> snd,
   loopers = map fst loop_tacs,