tuned blacklisting in relevance filter
authorblanchet
Sat Jan 05 11:24:09 2013 +0100 (2013-01-05 ago)
changeset 5073607dfdf72ab75
parent 50735 6b232d76cbc9
child 50737 f310d1735d93
tuned blacklisting in relevance filter
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Jan 04 21:56:20 2013 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sat Jan 05 11:24:09 2013 +0100
     1.3 @@ -141,10 +141,11 @@
     1.4  
     1.5  (* Reject theorems with names like "List.filter.filter_list_def" or
     1.6    "Accessible_Part.acc.defs", as these are definitions arising from packages. *)
     1.7 -fun is_package_def a =
     1.8 -  let val names = Long_Name.explode a in
     1.9 -    (length names > 2 andalso not (hd names = "local") andalso
    1.10 -     String.isSuffix "_def" a) orelse String.isSuffix "_defs" a
    1.11 +fun is_package_def s =
    1.12 +  let val ss = Long_Name.explode s in
    1.13 +    length ss > 2 andalso not (hd ss = "local") andalso
    1.14 +    exists (fn suf => String.isSuffix suf s)
    1.15 +           ["_case_def", "_rec_def", "_size_def", "_size_overloaded_def"]
    1.16    end
    1.17  
    1.18  (* FIXME: put other record thms here, or declare as "no_atp" *)
    1.19 @@ -189,10 +190,10 @@
    1.20  
    1.21  (* FIXME: Ad hoc list *)
    1.22  val technical_prefixes =
    1.23 -  ["ATP", "Code_Evaluation", "DSequence", "Enum", "Lazy_Sequence", "Meson",
    1.24 -   "Metis", "Nitpick", "New_DSequence", "New_Random_Sequence", "Quickcheck",
    1.25 -   "Quickcheck_Exhaustive", "Quickcheck_Narrowing", "Random_Sequence",
    1.26 -   "Sledgehammer", "SMT"]
    1.27 +  ["ATP", "Code_Evaluation", "Datatype", "DSequence", "Enum", "Lazy_Sequence",
    1.28 +   "Meson", "Metis", "Nitpick", "New_DSequence", "New_Random_Sequence",
    1.29 +   "Quickcheck", "Quickcheck_Exhaustive", "Quickcheck_Narrowing",
    1.30 +   "Random_Sequence", "Sledgehammer", "SMT"]
    1.31    |> map (suffix Long_Name.separator)
    1.32  
    1.33  fun has_technical_prefix s =