src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
changeset 48667 ac58317ef11f
parent 48530 d443166f9520
child 49981 e12b4e9794fd
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Aug 03 17:56:35 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Aug 03 17:56:35 2012 +0200
     1.3 @@ -182,14 +182,17 @@
     1.4    apply_depth t > max_apply_depth orelse
     1.5    (not ho_atp andalso formula_has_too_many_lambdas [] t)
     1.6  
     1.7 -(* These theories contain auxiliary facts that could positively confuse
     1.8 -   Sledgehammer if they were included. *)
     1.9 -val sledgehammer_prefixes =
    1.10 -  ["ATP", "Meson", "Metis", "Sledgehammer"] |> map (suffix Long_Name.separator)
    1.11 +(* FIXME: Ad hoc list *)
    1.12 +val technical_prefixes =
    1.13 +  ["ATP", "Code_Evaluation", "DSequence", "Enum", "Lazy_Sequence", "Meson",
    1.14 +   "Metis", "Nitpick", "New_DSequence", "New_Random_Sequence", "Quickcheck",
    1.15 +   "Quickcheck_Exhaustive", "Quickcheck_Narrowing", "Random_Sequence",
    1.16 +   "Sledgehammer", "SMT"]
    1.17 +  |> map (suffix Long_Name.separator)
    1.18  
    1.19 -val exists_sledgehammer_const =
    1.20 -  exists_Const (fn (s, _) =>
    1.21 -      exists (fn pref => String.isPrefix pref s) sledgehammer_prefixes)
    1.22 +fun has_technical_prefix s =
    1.23 +  exists (fn pref => String.isPrefix pref s) technical_prefixes
    1.24 +val exists_technical_const = exists_Const (has_technical_prefix o fst)
    1.25  
    1.26  (* FIXME: make more reliable *)
    1.27  val exists_low_level_class_const =
    1.28 @@ -224,9 +227,8 @@
    1.29    is_likely_tautology_or_too_meta th orelse
    1.30    let val t = prop_of th in
    1.31      is_formula_too_complex ho_atp t orelse
    1.32 -    exists_type type_has_top_sort t orelse
    1.33 -    exists_sledgehammer_const t orelse exists_low_level_class_const t orelse
    1.34 -    is_that_fact th
    1.35 +    exists_type type_has_top_sort t orelse exists_technical_const t orelse
    1.36 +    exists_low_level_class_const t orelse is_that_fact th
    1.37    end
    1.38  
    1.39  fun hackish_string_for_term thy t =