--- 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.*)