diff -r d4e9d6b7f48d -r 62616d8422c5 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>\expand_def\, lhss = ["x::'a"], proc = K get_def}; +val _ = \<^simproc_setup>\expand_def ("x::'a") = \K get_def\\; (* Isar command *)