diff -r 6d167422bcb0 -r 032a31db4c6f src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Fri Dec 22 17:19:08 2023 +0100
+++ b/src/Pure/Proof/extraction.ML	Fri Dec 22 21:03:16 2023 +0100
@@ -820,10 +820,9 @@
       in
         thy
         |> Sign.add_consts [(b, fastype_of ft, NoSyn)]
-        |> Global_Theory.add_defs false
-           [((Binding.qualified_name (Thm.def_name (extr_name s vs)),
-             Logic.mk_equals (head, ft)), [])]
-        |-> (fn [def_thm] =>
+        |> Global_Theory.add_def
+           (Binding.qualified_name (Thm.def_name (extr_name s vs)), Logic.mk_equals (head, ft))
+        |-> (fn def_thm =>
            Spec_Rules.add_global b Spec_Rules.equational
              [Thm.term_of (Thm.lhs_of def_thm)] [def_thm]
            #> Code.declare_default_eqns_global [(def_thm, true)])