Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Wed, 07 Aug 2024 20:07:50 +0200
changeset 80667 b167ec56056f
parent 80666 cdae621613da
child 80668 863b6699274e
tuned;
src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle