# HG changeset patch # User desharna # Date 1742919096 -3600 # Node ID 541370cb289dad071910bfa08131db3f712cad3c # Parent b1c40a1ae4a932db3e63d59b17497f902c025f71 tuned diff -r b1c40a1ae4a9 -r 541370cb289d src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Tue Mar 25 15:26:48 2025 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Tue Mar 25 17:11:36 2025 +0100 @@ -489,7 +489,7 @@ NONE => false | SOME ths' => eq_list Thm.eq_thm_prop (ths, ths')) in - snd (fold_rev (fn th0 => fn (j, accum) => + snd (fold_rev (fn th0 => fn (j, accum as {singletons, dotteds, collections}) => let val th = transfer th0 in (j - 1, if not (member Thm.eq_thm_prop add_ths th) andalso @@ -517,19 +517,23 @@ val stature = stature_of_thm global assms chained css name0 th val new = ((get_name, stature), th) in - (if collection then apsnd o apsnd - else if dotted_name then apsnd o apfst - else apfst) (cons new) accum + if collection then + {singletons = singletons, dotteds = dotteds, collections = new :: collections} + else if dotted_name then + {singletons = singletons, dotteds = new :: dotteds, collections = collections} + else + {singletons = new :: singletons, dotteds = dotteds, collections = collections} end) end) ths (n, accum)) end) + val {singletons, dotteds, collections} = + {singletons = [], dotteds = [], collections = []} + |> add_facts false fold local_facts (unnamed_locals @ named_locals) + |> add_facts true Facts.fold_static global_facts global_facts in (* Names like "xxx" are preferred to "xxx.yyy", which are preferred to "xxx(666)" and the like. "Preferred" means "put to the front of the list". *) - ([], ([], [])) - |> add_facts false fold local_facts (unnamed_locals @ named_locals) - |> add_facts true Facts.fold_static global_facts global_facts - ||> op @ |> op @ + singletons @ dotteds @ collections end fun nearly_all_facts ctxt inst_inducts {add, del, only} keywords css chained hyp_ts concl_t =