# HG changeset patch # User blanchet # Date 1272471071 -7200 # Node ID f8da913b6c3a366634d68a902cbd9243cb7644a3 # Parent d29617bcc1fbfe746599edfbf1c46e7c73818af7 make sure short theorem names are preferred to composite ones in Sledgehammer; this code used to work at some point diff -r d29617bcc1fb -r f8da913b6c3a src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Wed Apr 28 17:56:07 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Wed Apr 28 18:11:11 2010 +0200 @@ -392,13 +392,14 @@ fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a; -(*The single theorems go BEFORE the multiple ones. Blacklist is applied to all.*) +(* The single-name theorems go after the multiple-name ones, so that single + names are preferred when both are available. *) fun name_thm_pairs respect_no_atp ctxt = let val (mults, singles) = List.partition is_multi (all_valid_thms respect_no_atp ctxt) - val ps = [] |> fold add_multi_names mults - |> fold add_single_names singles + val ps = [] |> fold add_single_names singles + |> fold add_multi_names mults in ps |> respect_no_atp ? filter_out (No_ATPs.member ctxt o snd) end; fun check_named ("", th) =