# HG changeset patch
# User desharna
# Date 1642858415 -3600
# Node ID 01bb90de56bb88d04c950ac91a480a005ec8c653
# Parent  4106bc2a9cc8d348e145d97b1781cc2916b10d5d
optimized facts traversal in TPTP translation

diff -r 4106bc2a9cc8 -r 01bb90de56bb src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Sat Jan 22 14:00:36 2022 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Sat Jan 22 14:33:35 2022 +0100
@@ -2083,14 +2083,14 @@
 
     val hyp_ts = map freeze_term hyp_ts;
     val concl_t = freeze_term concl_t;
+    val maybe_presimp_prop = presimp ? presimp_prop simp_options ctxt type_enc
 
-    val facts = facts |> map (apsnd (pair Axiom))
+    val facts = facts |> map (apsnd (pair Axiom o maybe_presimp_prop))
     val conjs =
       map (pair prem_role) hyp_ts @ [(Conjecture, s_not_prop concl_t)]
-      |> map_index (apfst (rpair (Local, General) o string_of_int))
+      |> map_index (map_prod (rpair (Local, General) o string_of_int) (apsnd maybe_presimp_prop))
     val ((conjs, facts), lam_facts) =
       (conjs, facts)
-      |> presimp ? apply2 (map (apsnd (apsnd (presimp_prop simp_options ctxt type_enc))))
       |> (if lam_trans = no_lamsN then
             rpair []
           else