# HG changeset patch
# User wenzelm
# Date 1723054070 -7200
# Node ID b167ec56056f20b9b04ded4a36659a28de142ad5
# Parent  cdae621613daf6bed3d99093a210fada8552dce1
tuned;

diff -r cdae621613da -r b167ec56056f src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML	Wed Aug 07 20:06:55 2024 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML	Wed Aug 07 20:07:50 2024 +0200
@@ -417,9 +417,7 @@
     fold safe_instantiate_bound bindings' ([], HOLogic.dest_Trueprop orig_parent_fmla)
     |> snd (*discard var typing context*)
     |> close_formula
-    |> single
-    |> Type_Infer_Context.infer_types (Context.proof_of (Context.Theory thy))
-    |> the_single
+    |> singleton (Type_Infer_Context.infer_types (Context.proof_of (Context.Theory thy)))
     |> HOLogic.mk_Trueprop
     |> rpair bindings'
   end