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.
make sure short theorem names are preferred to composite ones in Sledgehammer;
authorblanchet
Wed, 28 Apr 2010 18:11:11 +0200
changeset 36550 f8da913b6c3a
parent 36549 d29617bcc1fb
child 36551 cc42df660808
make sure short theorem names are preferred to composite ones in Sledgehammer; this code used to work at some point
src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML file | annotate | diff | comparison | revisions 
--- 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) =
isabelle