diff -r d3328c562307 -r d769a183d51d src/Pure/ML/ml_thms.ML
--- a/src/Pure/ML/ml_thms.ML	Sat Oct 21 14:36:47 2023 +0200
+++ b/src/Pure/ML/ml_thms.ML	Sat Oct 21 21:19:02 2023 +0200
@@ -8,6 +8,8 @@
 sig
   val the_attributes: Proof.context -> int -> Token.src list
   val the_thmss: Proof.context -> thm list list
+  val thm_binding: string -> bool -> thm list -> Proof.context ->
+    (Proof.context -> string * string) * Proof.context
   val embedded_lemma: (Proof.context -> thm list * (term list * Proof.context)) parser
   val get_stored_thms: unit -> thm list
   val get_stored_thm: unit -> thm