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 =