# 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) =