diff -r 7849b6370425 -r 505f97165f52 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Fri Jul 19 11:29:05 2024 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Fri Jul 19 16:58:52 2024 +0200
@@ -16,7 +16,7 @@
 fun thm_name_of thm =
   (case Proofterm.fold_proof_atoms false (fn PThm ({thm_name, ...}, _) => cons thm_name | _ => I)
       [Thm.proof_of thm] [] of
-    [thm_name] => thm_name
+    [(thm_name, _)] => thm_name
   | _ => raise THM ("thm_name_of: bad proof of theorem", 0, [thm]));
 
 val short_name_of = Thm_Name.short o thm_name_of;