1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Jul 23 15:32:30 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Jul 23 15:32:30 2012 +0200
     1.3 @@ -49,9 +49,6 @@
     1.4     del : (Facts.ref * Attrib.src list) list,
     1.5     only : bool}
     1.6  
     1.7 -val sledgehammer_prefixes =
     1.8 -  ["ATP", "Meson", "Metis", "Sledgehammer"] |> map (suffix Long_Name.separator)
     1.9 -
    1.10  (* experimental features *)
    1.11  val ignore_no_atp =
    1.12    Attrib.setup_config_bool @{binding sledgehammer_ignore_no_atp} (K false)
    1.13 @@ -147,10 +144,11 @@
    1.14  fun multi_base_blacklist ctxt ho_atp =
    1.15    ["defs", "select_defs", "update_defs", "split", "splits", "split_asm",
    1.16     "cases", "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong",
    1.17 -   "weak_case_cong"]
    1.18 +   "weak_case_cong", "nibble_pair_of_char_simps", "nibble.simps",
    1.19 +   "nibble.distinct"]
    1.20    |> not (ho_atp orelse (Config.get ctxt instantiate_inducts)) ?
    1.21          append ["induct", "inducts"]
    1.22 -  |> map (prefix ".")
    1.23 +  |> map (prefix Long_Name.separator)
    1.24  
    1.25  val max_lambda_nesting = 3 (*only applies if not ho_atp*)
    1.26  
    1.27 @@ -182,6 +180,11 @@
    1.28    apply_depth t > max_apply_depth orelse
    1.29    (not ho_atp andalso formula_has_too_many_lambdas [] t)
    1.30  
    1.31 +(* These theories contain auxiliary facts that could positively confuse
    1.32 +   Sledgehammer if they were included. *)
    1.33 +val sledgehammer_prefixes =
    1.34 +  ["ATP", "Meson", "Metis", "Sledgehammer"] |> map (suffix Long_Name.separator)
    1.35 +
    1.36  val exists_sledgehammer_const =
    1.37    exists_Const (fn (s, _) =>
    1.38        exists (fn pref => String.isPrefix pref s) sledgehammer_prefixes)

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Jul 23 15:32:30 2012 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Jul 23 15:32:30 2012 +0200
     2.3 @@ -316,7 +316,7 @@
     2.4  
     2.5  (* Too many dependencies is a sign that a decision procedure is at work. There
     2.6     isn't much too learn from such proofs. *)
     2.7 -val max_dependencies = 15
     2.8 +val max_dependencies = 20
     2.9  val atp_dependency_default_max_fact = 50
    2.10  
    2.11  (* "type_definition_xxx" facts are characterized by their use of "CollectI". *)
    2.12 @@ -689,6 +689,14 @@
    2.13            (true, "")
    2.14          end)
    2.15  
    2.16 +val evil_theories =
    2.17 +  ["Code_Evaluation", "DSequence", "Enum", "Lazy_Sequence", "Nitpick",
    2.18 +   "New_DSequence", "New_Random_Sequence", "Quickcheck",
    2.19 +   "Quickcheck_Exhaustive", "Quickcheck_Narrowing", "Random_Sequence", "SMT"]
    2.20 +
    2.21 +fun fact_has_evil_theory (_, th) =
    2.22 +  member (op =) evil_theories (Context.theory_name (theory_of_thm th))
    2.23 +
    2.24  fun sendback sub =
    2.25    Markup.markup Isabelle_Markup.sendback (sledgehammerN ^ " " ^ sub)
    2.26  
    2.27 @@ -703,7 +711,8 @@
    2.28        Time.+ (Timer.checkRealTimer timer, commit_timeout)
    2.29      val {fact_G} = mash_get ctxt
    2.30      val (old_facts, new_facts) =
    2.31 -      facts |> List.partition (is_fact_in_graph fact_G)
    2.32 +      facts |> filter_out fact_has_evil_theory
    2.33 +            |> List.partition (is_fact_in_graph fact_G)
    2.34              ||> sort (thm_ord o pairself snd)
    2.35    in
    2.36      if null new_facts andalso (not atp orelse null old_facts) then