--- 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