diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML	Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML	Sun Aug 04 17:39:47 2024 +0200
@@ -313,7 +313,7 @@
                 then should still be able to handle formulas like
                 (! X, X. F).*)
               if x = bound_var andalso
-                 fst (dest_Const t1) = \<^const_name>\<open>All\<close> then
+                 dest_Const_name t1 = \<^const_name>\<open>All\<close> then
                   (*Body might contain free variables, so bind them using "var_ctxt".
                     this involves replacing instances of Free with instances of Bound
                     at the right index.*)