# HG changeset patch
# User wenzelm
# Date 1697727999 -7200
# Node ID 0b3700d317588b715f3d162ee8240eb3f66beab8
# Parent  807b249f1061a37c007bfe395a8400f4f75a6b70
clarified signature;

diff -r 807b249f1061 -r 0b3700d31758 src/HOL/Analysis/measurable.ML
--- a/src/HOL/Analysis/measurable.ML	Thu Oct 19 16:31:17 2023 +0200
+++ b/src/HOL/Analysis/measurable.ML	Thu Oct 19 17:06:39 2023 +0200
@@ -22,7 +22,7 @@
 
   val measurable_tac : Proof.context -> thm list -> tactic
 
-  val simproc : Proof.context -> cterm -> thm option
+  val simproc : Simplifier.proc
 
   val add_preprocessor : string -> preprocessor -> Context.generic -> Context.generic
   val del_preprocessor : string -> Context.generic -> Context.generic
diff -r 807b249f1061 -r 0b3700d31758 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu Oct 19 16:31:17 2023 +0200
+++ b/src/HOL/HOL.thy	Thu Oct 19 17:06:39 2023 +0200
@@ -1648,7 +1648,7 @@
 signature REORIENT_PROC =
 sig
   val add : (term -> bool) -> theory -> theory
-  val proc : Proof.context -> cterm -> thm option
+  val proc : Simplifier.proc
 end;
 
 structure Reorient_Proc : REORIENT_PROC =
diff -r 807b249f1061 -r 0b3700d31758 src/HOL/HOLCF/Tools/cont_proc.ML
--- a/src/HOL/HOLCF/Tools/cont_proc.ML	Thu Oct 19 16:31:17 2023 +0200
+++ b/src/HOL/HOLCF/Tools/cont_proc.ML	Thu Oct 19 17:06:39 2023 +0200
@@ -8,7 +8,7 @@
   val cont_thms: term -> thm list
   val all_cont_thms: term -> thm list
   val cont_tac: Proof.context -> int -> tactic
-  val cont_proc: Proof.context -> cterm -> thm option
+  val cont_proc: Simplifier.proc
 end
 
 structure ContProc : CONT_PROC =
diff -r 807b249f1061 -r 0b3700d31758 src/HOL/Library/Cancellation/cancel.ML
--- a/src/HOL/Library/Cancellation/cancel.ML	Thu Oct 19 16:31:17 2023 +0200
+++ b/src/HOL/Library/Cancellation/cancel.ML	Thu Oct 19 17:06:39 2023 +0200
@@ -35,7 +35,7 @@
 
 signature CANCEL =
 sig
-  val proc: Proof.context -> cterm -> thm option
+  val proc: Simplifier.proc
 end;
 
 functor Cancel_Fun(Data: CANCEL_NUMERALS_DATA): CANCEL =
diff -r 807b249f1061 -r 0b3700d31758 src/HOL/Library/Cancellation/cancel_simprocs.ML
--- a/src/HOL/Library/Cancellation/cancel_simprocs.ML	Thu Oct 19 16:31:17 2023 +0200
+++ b/src/HOL/Library/Cancellation/cancel_simprocs.ML	Thu Oct 19 17:06:39 2023 +0200
@@ -7,10 +7,10 @@
 
 signature CANCEL_SIMPROCS =
 sig
-  val eq_cancel: Proof.context -> cterm -> thm option
-  val less_cancel: Proof.context -> cterm -> thm option
-  val less_eq_cancel: Proof.context -> cterm -> thm option
-  val diff_cancel: Proof.context -> cterm -> thm option
+  val eq_cancel: Simplifier.proc
+  val less_cancel: Simplifier.proc
+  val less_eq_cancel: Simplifier.proc
+  val diff_cancel: Simplifier.proc
 end;
 
 structure Cancel_Simprocs : CANCEL_SIMPROCS =
diff -r 807b249f1061 -r 0b3700d31758 src/HOL/Library/multiset_simprocs.ML
--- a/src/HOL/Library/multiset_simprocs.ML	Thu Oct 19 16:31:17 2023 +0200
+++ b/src/HOL/Library/multiset_simprocs.ML	Thu Oct 19 17:06:39 2023 +0200
@@ -7,8 +7,8 @@
 
 signature MULTISET_SIMPROCS =
 sig
-  val subset_cancel_msets: Proof.context -> cterm -> thm option
-  val subseteq_cancel_msets: Proof.context -> cterm -> thm option
+  val subset_cancel_msets: Simplifier.proc
+  val subseteq_cancel_msets: Simplifier.proc
 end;
 
 structure Multiset_Simprocs : MULTISET_SIMPROCS =
diff -r 807b249f1061 -r 0b3700d31758 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Oct 19 16:31:17 2023 +0200
+++ b/src/HOL/List.thy	Thu Oct 19 17:06:39 2023 +0200
@@ -557,7 +557,7 @@
 
 signature LIST_TO_SET_COMPREHENSION =
 sig
-  val simproc : Proof.context -> cterm -> thm option
+  val simproc : Simplifier.proc
 end
 
 structure List_to_Set_Comprehension : LIST_TO_SET_COMPREHENSION =
diff -r 807b249f1061 -r 0b3700d31758 src/HOL/Tools/SMT/z3_replay_rules.ML
--- a/src/HOL/Tools/SMT/z3_replay_rules.ML	Thu Oct 19 16:31:17 2023 +0200
+++ b/src/HOL/Tools/SMT/z3_replay_rules.ML	Thu Oct 19 17:06:39 2023 +0200
@@ -6,7 +6,7 @@
 
 signature Z3_REPLAY_RULES =
 sig
-  val apply: Proof.context -> cterm -> thm option
+  val apply: Simplifier.proc
 end;
 
 structure Z3_Replay_Rules: Z3_REPLAY_RULES =
diff -r 807b249f1061 -r 0b3700d31758 src/HOL/Tools/datatype_simprocs.ML
--- a/src/HOL/Tools/datatype_simprocs.ML	Thu Oct 19 16:31:17 2023 +0200
+++ b/src/HOL/Tools/datatype_simprocs.ML	Thu Oct 19 17:06:39 2023 +0200
@@ -6,7 +6,7 @@
 *)
 
 signature DATATYPE_SIMPROCS = sig
-  val no_proper_subterm_simproc : Proof.context -> cterm -> thm option
+  val no_proper_subterm_simproc : Simplifier.proc
 end
 
 structure Datatype_Simprocs : DATATYPE_SIMPROCS = struct
diff -r 807b249f1061 -r 0b3700d31758 src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Thu Oct 19 16:31:17 2023 +0200
+++ b/src/HOL/Tools/lin_arith.ML	Thu Oct 19 17:06:39 2023 +0200
@@ -9,7 +9,7 @@
   val pre_tac: Proof.context -> int -> tactic
   val simple_tac: Proof.context -> int -> tactic
   val tac: Proof.context -> int -> tactic
-  val simproc: Proof.context -> cterm -> thm option
+  val simproc: Simplifier.proc
   val add_inj_thms: thm list -> Context.generic -> Context.generic
   val add_lessD: thm -> Context.generic -> Context.generic
   val add_simps: thm list -> Context.generic -> Context.generic
diff -r 807b249f1061 -r 0b3700d31758 src/HOL/Tools/nat_numeral_simprocs.ML
--- a/src/HOL/Tools/nat_numeral_simprocs.ML	Thu Oct 19 16:31:17 2023 +0200
+++ b/src/HOL/Tools/nat_numeral_simprocs.ML	Thu Oct 19 17:06:39 2023 +0200
@@ -5,21 +5,21 @@
 
 signature NAT_NUMERAL_SIMPROCS =
 sig
-  val combine_numerals: Proof.context -> cterm -> thm option
-  val eq_cancel_numerals: Proof.context -> cterm -> thm option
-  val less_cancel_numerals: Proof.context -> cterm -> thm option
-  val le_cancel_numerals: Proof.context -> cterm -> thm option
-  val diff_cancel_numerals: Proof.context -> cterm -> thm option
-  val eq_cancel_numeral_factor: Proof.context -> cterm -> thm option
-  val less_cancel_numeral_factor: Proof.context -> cterm -> thm option
-  val le_cancel_numeral_factor: Proof.context -> cterm -> thm option
-  val div_cancel_numeral_factor: Proof.context -> cterm -> thm option
-  val dvd_cancel_numeral_factor: Proof.context -> cterm -> thm option
-  val eq_cancel_factor: Proof.context -> cterm -> thm option
-  val less_cancel_factor: Proof.context -> cterm -> thm option
-  val le_cancel_factor: Proof.context -> cterm -> thm option
-  val div_cancel_factor: Proof.context -> cterm -> thm option
-  val dvd_cancel_factor: Proof.context -> cterm -> thm option
+  val combine_numerals: Simplifier.proc
+  val eq_cancel_numerals: Simplifier.proc
+  val less_cancel_numerals: Simplifier.proc
+  val le_cancel_numerals: Simplifier.proc
+  val diff_cancel_numerals: Simplifier.proc
+  val eq_cancel_numeral_factor: Simplifier.proc
+  val less_cancel_numeral_factor: Simplifier.proc
+  val le_cancel_numeral_factor: Simplifier.proc
+  val div_cancel_numeral_factor: Simplifier.proc
+  val dvd_cancel_numeral_factor: Simplifier.proc
+  val eq_cancel_factor: Simplifier.proc
+  val less_cancel_factor: Simplifier.proc
+  val le_cancel_factor: Simplifier.proc
+  val div_cancel_factor: Simplifier.proc
+  val dvd_cancel_factor: Simplifier.proc
 end;
 
 structure Nat_Numeral_Simprocs : NAT_NUMERAL_SIMPROCS =
diff -r 807b249f1061 -r 0b3700d31758 src/HOL/Tools/numeral_simprocs.ML
--- a/src/HOL/Tools/numeral_simprocs.ML	Thu Oct 19 16:31:17 2023 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML	Thu Oct 19 17:06:39 2023 +0200
@@ -17,24 +17,24 @@
 signature NUMERAL_SIMPROCS =
 sig
   val trans_tac: Proof.context -> thm option -> tactic
-  val assoc_fold: Proof.context -> cterm -> thm option
-  val combine_numerals: Proof.context -> cterm -> thm option
-  val eq_cancel_numerals: Proof.context -> cterm -> thm option
-  val less_cancel_numerals: Proof.context -> cterm -> thm option
-  val le_cancel_numerals: Proof.context -> cterm -> thm option
-  val eq_cancel_factor: Proof.context -> cterm -> thm option
-  val le_cancel_factor: Proof.context -> cterm -> thm option
-  val less_cancel_factor: Proof.context -> cterm -> thm option
-  val div_cancel_factor: Proof.context -> cterm -> thm option
-  val mod_cancel_factor: Proof.context -> cterm -> thm option
-  val dvd_cancel_factor: Proof.context -> cterm -> thm option
-  val divide_cancel_factor: Proof.context -> cterm -> thm option
-  val eq_cancel_numeral_factor: Proof.context -> cterm -> thm option
-  val less_cancel_numeral_factor: Proof.context -> cterm -> thm option
-  val le_cancel_numeral_factor: Proof.context -> cterm -> thm option
-  val div_cancel_numeral_factor: Proof.context -> cterm -> thm option
-  val divide_cancel_numeral_factor: Proof.context -> cterm -> thm option
-  val field_combine_numerals: Proof.context -> cterm -> thm option
+  val assoc_fold: Simplifier.proc
+  val combine_numerals: Simplifier.proc
+  val eq_cancel_numerals: Simplifier.proc
+  val less_cancel_numerals: Simplifier.proc
+  val le_cancel_numerals: Simplifier.proc
+  val eq_cancel_factor: Simplifier.proc
+  val le_cancel_factor: Simplifier.proc
+  val less_cancel_factor: Simplifier.proc
+  val div_cancel_factor: Simplifier.proc
+  val mod_cancel_factor: Simplifier.proc
+  val dvd_cancel_factor: Simplifier.proc
+  val divide_cancel_factor: Simplifier.proc
+  val eq_cancel_numeral_factor: Simplifier.proc
+  val less_cancel_numeral_factor: Simplifier.proc
+  val le_cancel_numeral_factor: Simplifier.proc
+  val div_cancel_numeral_factor: Simplifier.proc
+  val divide_cancel_numeral_factor: Simplifier.proc
+  val field_combine_numerals: Simplifier.proc
   val field_divide_cancel_numeral_factor: simproc
   val num_ss: simpset
   val field_comp_conv: Proof.context -> conv
diff -r 807b249f1061 -r 0b3700d31758 src/HOL/Tools/set_comprehension_pointfree.ML
--- a/src/HOL/Tools/set_comprehension_pointfree.ML	Thu Oct 19 16:31:17 2023 +0200
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Thu Oct 19 17:06:39 2023 +0200
@@ -7,9 +7,9 @@
 
 signature SET_COMPREHENSION_POINTFREE =
 sig
-  val base_simproc : Proof.context -> cterm -> thm option
-  val code_simproc : Proof.context -> cterm -> thm option
-  val simproc : Proof.context -> cterm -> thm option
+  val base_simproc : Simplifier.proc
+  val code_simproc : Simplifier.proc
+  val simproc : Simplifier.proc
 end
 
 structure Set_Comprehension_Pointfree : SET_COMPREHENSION_POINTFREE =
diff -r 807b249f1061 -r 0b3700d31758 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Thu Oct 19 16:31:17 2023 +0200
+++ b/src/HOL/Transcendental.thy	Thu Oct 19 17:06:39 2023 +0200
@@ -7352,9 +7352,9 @@
 val sqrt' : int option -> int -> int option
 val nth_root : int option -> int -> int -> int option
 val nth_root' : int option -> int -> int -> int option
-val sqrt_simproc : Proof.context -> cterm -> thm option
-val root_simproc : int * int -> Proof.context -> cterm -> thm option
-val powr_simproc : int * int -> Proof.context -> cterm -> thm option
+val sqrt_simproc : Simplifier.proc
+val root_simproc : int * int -> Simplifier.proc
+val powr_simproc : int * int -> Simplifier.proc
 
 end
 
diff -r 807b249f1061 -r 0b3700d31758 src/Provers/Arith/cancel_div_mod.ML
--- a/src/Provers/Arith/cancel_div_mod.ML	Thu Oct 19 16:31:17 2023 +0200
+++ b/src/Provers/Arith/cancel_div_mod.ML	Thu Oct 19 17:06:39 2023 +0200
@@ -27,7 +27,7 @@
 
 signature CANCEL_DIV_MOD =
 sig
-  val proc: Proof.context -> cterm -> thm option
+  val proc: Simplifier.proc
 end;
 
 
diff -r 807b249f1061 -r 0b3700d31758 src/Provers/Arith/cancel_numeral_factor.ML
--- a/src/Provers/Arith/cancel_numeral_factor.ML	Thu Oct 19 16:31:17 2023 +0200
+++ b/src/Provers/Arith/cancel_numeral_factor.ML	Thu Oct 19 17:06:39 2023 +0200
@@ -37,7 +37,7 @@
 
 
 functor CancelNumeralFactorFun(Data: CANCEL_NUMERAL_FACTOR_DATA):
-  sig val proc: Proof.context -> cterm -> thm option end =
+  sig val proc: Simplifier.proc end =
 struct
 
 (*the simplification procedure*)
diff -r 807b249f1061 -r 0b3700d31758 src/Provers/Arith/cancel_numerals.ML
--- a/src/Provers/Arith/cancel_numerals.ML	Thu Oct 19 16:31:17 2023 +0200
+++ b/src/Provers/Arith/cancel_numerals.ML	Thu Oct 19 17:06:39 2023 +0200
@@ -44,7 +44,7 @@
 
 signature CANCEL_NUMERALS =
 sig
-  val proc: Proof.context -> cterm -> thm option
+  val proc: Simplifier.proc
 end;
 
 functor CancelNumeralsFun(Data: CANCEL_NUMERALS_DATA): CANCEL_NUMERALS =
diff -r 807b249f1061 -r 0b3700d31758 src/Provers/Arith/combine_numerals.ML
--- a/src/Provers/Arith/combine_numerals.ML	Thu Oct 19 16:31:17 2023 +0200
+++ b/src/Provers/Arith/combine_numerals.ML	Thu Oct 19 17:06:39 2023 +0200
@@ -38,7 +38,7 @@
 
 functor CombineNumeralsFun(Data: COMBINE_NUMERALS_DATA):
   sig
-  val proc: Proof.context -> cterm -> thm option
+  val proc: Simplifier.proc
   end
 =
 struct
diff -r 807b249f1061 -r 0b3700d31758 src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Thu Oct 19 16:31:17 2023 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML	Thu Oct 19 17:06:39 2023 +0200
@@ -93,7 +93,7 @@
 sig
   val prems_lin_arith_tac: Proof.context -> int -> tactic
   val lin_arith_tac: Proof.context -> int -> tactic
-  val lin_arith_simproc: Proof.context -> cterm -> thm option
+  val lin_arith_simproc: Simplifier.proc
   val map_data:
     ({add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
       lessD: thm list, neqE: thm list, simpset: simpset,
diff -r 807b249f1061 -r 0b3700d31758 src/Provers/quantifier1.ML
--- a/src/Provers/quantifier1.ML	Thu Oct 19 16:31:17 2023 +0200
+++ b/src/Provers/quantifier1.ML	Thu Oct 19 17:06:39 2023 +0200
@@ -65,12 +65,12 @@
 
 signature QUANTIFIER1 =
 sig
-  val rearrange_all: Proof.context -> cterm -> thm option
-  val rearrange_All: Proof.context -> cterm -> thm option
-  val rearrange_Ball: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option
-  val rearrange_Ex: Proof.context -> cterm -> thm option
-  val rearrange_Bex: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option
-  val rearrange_Collect: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option
+  val rearrange_all: Simplifier.proc
+  val rearrange_All: Simplifier.proc
+  val rearrange_Ball: (Proof.context -> tactic) -> Simplifier.proc
+  val rearrange_Ex: Simplifier.proc
+  val rearrange_Bex: (Proof.context -> tactic) -> Simplifier.proc
+  val rearrange_Collect: (Proof.context -> tactic) -> Simplifier.proc
 end;
 
 functor Quantifier1(Data: QUANTIFIER1_DATA): QUANTIFIER1 =
diff -r 807b249f1061 -r 0b3700d31758 src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Thu Oct 19 16:31:17 2023 +0200
+++ b/src/Pure/raw_simplifier.ML	Thu Oct 19 17:06:39 2023 +0200
@@ -19,7 +19,8 @@
   type rrule
   val mk_rrules: Proof.context -> thm list -> rrule list
   val eq_rrule: rrule * rrule -> bool
-  type proc
+  type proc = Proof.context -> cterm -> thm option
+  type simproc0
   type solver
   val mk_solver: string -> (Proof.context -> int -> tactic) -> solver
   type simpset
@@ -36,8 +37,7 @@
   val dest_simps: simpset -> thm list
   type simproc
   val eq_simproc: simproc * simproc -> bool
-  val cert_simproc: theory -> string ->
-    {lhss: term list, proc: (Proof.context -> cterm -> thm option) Morphism.entity} -> simproc
+  val cert_simproc: theory -> string -> {lhss: term list, proc: proc Morphism.entity} -> simproc
   val transform_simproc: morphism -> simproc -> simproc
   val trim_context_simproc: simproc -> simproc
   val simpset_of: Proof.context -> simpset
@@ -208,14 +208,17 @@
 
 (* simplification procedures *)
 
-datatype proc =
-  Proc of
+type proc = Proof.context -> cterm -> thm option;
+
+datatype simproc0 =
+  Simproc0 of
    {name: string,
     lhs: term,
-    proc: (Proof.context -> cterm -> thm option) Morphism.entity,
+    proc: proc Morphism.entity,
     stamp: stamp};
 
-fun eq_proc (Proc {stamp = stamp1, ...}, Proc {stamp = stamp2, ...}) = stamp1 = stamp2;
+fun eq_simproc0 (Simproc0 {stamp = stamp1, ...}, Simproc0 {stamp = stamp2, ...}) =
+  stamp1 = stamp2;
 
 
 (* solvers *)
@@ -257,7 +260,7 @@
     prems: thm list,
     depth: int * bool Unsynchronized.ref} *
    {congs: thm Congtab.table * cong_name list,
-    procs: proc Net.net,
+    procs: simproc0 Net.net,
     mk_rews:
      {mk: Proof.context -> thm -> thm list,
       mk_cong: Proof.context -> thm -> thm,
@@ -288,7 +291,7 @@
  {simps = Net.entries rules
     |> map (fn {name, thm, ...} => (name, thm)),
   procs = Net.entries procs
-    |> map (fn Proc {name, lhs, stamp, ...} => ((name, lhs), stamp))
+    |> map (fn Simproc0 {name, lhs, stamp, ...} => ((name, lhs), stamp))
     |> partition_eq (eq_snd op =)
     |> map (fn ps => (fst (fst (hd ps)), map (snd o fst) ps)),
   congs = congs |> fst |> Congtab.dest,
@@ -336,7 +339,7 @@
       val depth' = if #1 depth1 < #1 depth2 then depth2 else depth1;
       val congs' = Congtab.merge (K true) (congs1, congs2);
       val weak' = merge (op =) (weak1, weak2);
-      val procs' = Net.merge eq_proc (procs1, procs2);
+      val procs' = Net.merge eq_simproc0 (procs1, procs2);
       val loop_tacs' = AList.merge (op =) (K true) (loop_tacs1, loop_tacs2);
       val unsafe_solvers' = merge eq_solver (unsafe_solvers1, unsafe_solvers2);
       val solvers' = merge eq_solver (solvers1, solvers2);
@@ -715,7 +718,7 @@
   Simproc of
     {name: string,
      lhss: term list,
-     proc: (Proof.context -> cterm -> thm option) Morphism.entity,
+     proc: proc Morphism.entity,
      stamp: stamp};
 
 fun eq_simproc (Simproc {stamp = stamp1, ...}, Simproc {stamp = stamp2, ...}) = stamp1 = stamp2;
@@ -739,28 +742,28 @@
 
 local
 
-fun add_proc (proc as Proc {name, lhs, ...}) ctxt =
+fun add_proc (proc as Simproc0 {name, lhs, ...}) ctxt =
  (cond_tracing ctxt (fn () =>
     print_term ctxt ("Adding simplification procedure " ^ quote name ^ " for") lhs);
   ctxt |> map_simpset2
     (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) =>
-      (congs, Net.insert_term eq_proc (lhs, proc) procs,
+      (congs, Net.insert_term eq_simproc0 (lhs, proc) procs,
         mk_rews, term_ord, subgoal_tac, loop_tacs, solvers))
   handle Net.INSERT =>
     (cond_warning ctxt (fn () => "Ignoring duplicate simplification procedure " ^ quote name);
       ctxt));
 
-fun del_proc (proc as Proc {name, lhs, ...}) ctxt =
+fun del_proc (proc as Simproc0 {name, lhs, ...}) ctxt =
   ctxt |> map_simpset2
     (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) =>
-      (congs, Net.delete_term eq_proc (lhs, proc) procs,
+      (congs, Net.delete_term eq_simproc0 (lhs, proc) procs,
         mk_rews, term_ord, subgoal_tac, loop_tacs, solvers))
   handle Net.DELETE =>
     (cond_warning ctxt (fn () => "Simplification procedure " ^ quote name ^ " not in simpset");
       ctxt);
 
 fun prep_procs (Simproc {name, lhss, proc, stamp}) =
-  lhss |> map (fn lhs => Proc {name = name, lhs = lhs, proc = proc, stamp = stamp});
+  lhss |> map (fn lhs => Simproc0 {name = name, lhs = lhs, proc = proc, stamp = stamp});
 
 in
 
@@ -1049,7 +1052,7 @@
       in sort rrs ([], []) end;
 
     fun proc_rews [] = NONE
-      | proc_rews (Proc {name, proc, lhs, ...} :: ps) =
+      | proc_rews (Simproc0 {name, proc, lhs, ...} :: ps) =
           if Pattern.matches (Proof_Context.theory_of ctxt) (lhs, Thm.term_of t) then
             (cond_tracing' ctxt simp_debug (fn () =>
               print_term ctxt ("Trying procedure " ^ quote name ^ " on:") eta_t);
diff -r 807b249f1061 -r 0b3700d31758 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Thu Oct 19 16:31:17 2023 +0200
+++ b/src/Pure/simplifier.ML	Thu Oct 19 17:06:39 2023 +0200
@@ -38,14 +38,13 @@
   val check_simproc: Proof.context -> xstring * Position.T -> string * simproc
   val the_simproc: Proof.context -> string -> simproc
   val make_simproc: Proof.context -> string ->
-    {lhss: term list, proc: morphism -> Proof.context -> cterm -> thm option} -> simproc
-  type 'a simproc_spec =
-    {passive: bool, lhss: 'a list, proc: morphism -> Proof.context -> cterm -> thm option}
+    {lhss: term list, proc: morphism -> proc} -> simproc
+  type 'a simproc_spec = {passive: bool, lhss: 'a list, proc: morphism -> proc}
   val define_simproc: binding -> term simproc_spec -> local_theory -> simproc * local_theory
   val define_simproc_cmd: binding -> string simproc_spec -> local_theory -> simproc * local_theory
   type 'a simproc_setup = {passive: bool, name: binding, lhss: string list, proc: 'a}
   type simproc_setup_input = Input.source simproc_setup
-  type simproc_setup_internal = (morphism -> Proof.context -> cterm -> thm option) simproc_setup
+  type simproc_setup_internal = (morphism -> proc) simproc_setup
   val simproc_setup_parser: Input.source simproc_setup parser
   val simproc_setup_ml: Input.source simproc_setup -> ML_Lex.token Antiquote.antiquote list
   val simproc_setup: simproc_setup_internal -> simproc
@@ -140,7 +139,7 @@
 type 'a simproc_spec =
  {passive: bool,
   lhss: 'a list,
-  proc: morphism -> Proof.context -> cterm -> thm option};
+  proc: morphism -> proc};
 
 local
 
@@ -174,7 +173,7 @@
 
 type 'a simproc_setup = {passive: bool, name: binding, lhss: string list, proc: 'a};
 type simproc_setup_input = Input.source simproc_setup;
-type simproc_setup_internal = (morphism -> Proof.context -> cterm -> thm option) simproc_setup;
+type simproc_setup_internal = (morphism -> proc) simproc_setup;
 
 val simproc_setup_parser : simproc_setup_input parser =
   Scan.optional (Parse.$$$ "passive" >> K true) false --
diff -r 807b249f1061 -r 0b3700d31758 src/ZF/Datatype.thy
--- a/src/ZF/Datatype.thy	Thu Oct 19 16:31:17 2023 +0200
+++ b/src/ZF/Datatype.thy	Thu Oct 19 17:06:39 2023 +0200
@@ -63,7 +63,7 @@
 structure Data_Free:
 sig
   val trace: bool Config.T
-  val proc: Proof.context -> cterm -> thm option
+  val proc: Simplifier.proc
 end =
 struct
 
diff -r 807b249f1061 -r 0b3700d31758 src/ZF/arith_data.ML
--- a/src/ZF/arith_data.ML	Thu Oct 19 16:31:17 2023 +0200
+++ b/src/ZF/arith_data.ML	Thu Oct 19 17:06:39 2023 +0200
@@ -7,9 +7,9 @@
 signature ARITH_DATA =
 sig
   (*the main outcome*)
-  val nateq_cancel_numerals_proc: Proof.context -> cterm -> thm option
-  val natless_cancel_numerals_proc: Proof.context -> cterm -> thm option
-  val natdiff_cancel_numerals_proc: Proof.context -> cterm -> thm option
+  val nateq_cancel_numerals_proc: Simplifier.proc
+  val natless_cancel_numerals_proc: Simplifier.proc
+  val natdiff_cancel_numerals_proc: Simplifier.proc
   (*tools for use in similar applications*)
   val gen_trans_tac: Proof.context -> thm -> thm option -> tactic
   val prove_conv: string -> tactic list -> Proof.context -> thm list -> term * term -> thm option
diff -r 807b249f1061 -r 0b3700d31758 src/ZF/int_arith.ML
--- a/src/ZF/int_arith.ML	Thu Oct 19 16:31:17 2023 +0200
+++ b/src/ZF/int_arith.ML	Thu Oct 19 17:06:39 2023 +0200
@@ -6,11 +6,11 @@
 
 signature INT_NUMERAL_SIMPROCS =
 sig
-  val inteq_cancel_numerals_proc: Proof.context -> cterm -> thm option
-  val intless_cancel_numerals_proc: Proof.context -> cterm -> thm option
-  val intle_cancel_numerals_proc: Proof.context -> cterm -> thm option
-  val int_combine_numerals_proc: Proof.context -> cterm -> thm option
-  val int_combine_numerals_prod_proc: Proof.context -> cterm -> thm option
+  val inteq_cancel_numerals_proc: Simplifier.proc
+  val intless_cancel_numerals_proc: Simplifier.proc
+  val intle_cancel_numerals_proc: Simplifier.proc
+  val int_combine_numerals_proc: Simplifier.proc
+  val int_combine_numerals_prod_proc: Simplifier.proc
 end
 
 structure Int_Numeral_Simprocs: INT_NUMERAL_SIMPROCS =