diff -r f6d2679ab6c1 -r 64973b03b778 src/HOL/Decision_Procs/langford.ML
--- a/src/HOL/Decision_Procs/langford.ML	Sat Oct 21 00:25:40 2023 +0200
+++ b/src/HOL/Decision_Procs/langford.ML	Sat Oct 21 11:24:34 2023 +0200
@@ -127,7 +127,7 @@
 
 local
 
-fun proc ctxt ct =
+fun reduce_ex_proc ctxt ct =
   (case Thm.term_of ct of
     \<^Const_>\<open>Ex _ for \<open>Abs _\<close>\<close> =>
       let
@@ -168,9 +168,7 @@
 
 in
 
-val reduce_ex_simproc =
-  Simplifier.make_simproc \<^context> "reduce_ex_simproc"
-    {lhss = [\<^term>\<open>\<exists>x. P x\<close>], proc = K proc};
+val reduce_ex_simproc = \<^simproc_setup>\<open>passive reduce_ex ("\<exists>x. P x") = \<open>K reduce_ex_proc\<close>\<close>;
 
 end;