src/Pure/ex/Def.thy

--- a/src/Pure/ex/Def.thy	Fri Oct 20 16:40:41 2023 +0200
+++ b/src/Pure/ex/Def.thy	Fri Oct 20 22:19:05 2023 +0200
@@ -65,9 +65,7 @@
 
 (* simproc setup *)
 
-val _ =
-  Simplifier.simproc_setup
-    {passive = false, name = \<^binding>\<open>expand_def\<close>, lhss = ["x::'a"], proc = K get_def};
+val _ = \<^simproc_setup>\<open>expand_def ("x::'a") = \<open>K get_def\<close>\<close>;
 
 
 (* Isar command *)