1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu Mar 17 09:58:13 2011 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu Mar 17 11:18:31 2011 +0100
     1.3 @@ -40,8 +40,8 @@
     1.4      Proof.context -> unit Symtab.table -> thm list
     1.5      -> Facts.ref * Attrib.src list -> ((string * locality) * thm) list
     1.6    val all_facts :
     1.7 -    Proof.context -> 'a Symtab.table -> bool -> relevance_fudge -> thm list
     1.8 -    -> thm list -> (((unit -> string) * locality) * (bool * thm)) list
     1.9 +    Proof.context -> 'a Symtab.table -> bool -> bool -> relevance_fudge
    1.10 +    -> thm list -> thm list -> (((unit -> string) * locality) * (bool * thm)) list
    1.11    val const_names_in_fact :
    1.12      theory -> (string * typ -> term list -> bool * term list) -> term
    1.13      -> string list
    1.14 @@ -793,7 +793,7 @@
    1.15      val simps = ctxt |> simpset_of |> dest_ss |> #simps |> map snd
    1.16    in (mk_fact_table I intros, mk_fact_table I elims, mk_fact_table I simps) end
    1.17  
    1.18 -fun all_facts ctxt reserved no_dangerous_types
    1.19 +fun all_facts ctxt reserved really_all no_dangerous_types
    1.20                ({intro_bonus, elim_bonus, simp_bonus, ...} : relevance_fudge)
    1.21                add_ths chained_ths =
    1.22    let
    1.23 @@ -819,7 +819,7 @@
    1.24        Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
    1.25      fun add_facts global foldx facts =
    1.26        foldx (fn (name0, ths) =>
    1.27 -        if name0 <> "" andalso
    1.28 +        if not really_all andalso name0 <> "" andalso
    1.29             forall (not o member Thm.eq_thm add_ths) ths andalso
    1.30             (Facts.is_concealed facts name0 orelse
    1.31              (respect_no_atp andalso is_package_def name0) orelse
    1.32 @@ -901,7 +901,8 @@
    1.33           maps (map (fn ((name, loc), th) => ((K name, loc), (true, th)))
    1.34                 o fact_from_ref ctxt reserved chained_ths) add
    1.35         else
    1.36 -         all_facts ctxt reserved no_dangerous_types fudge add_ths chained_ths)
    1.37 +         all_facts ctxt reserved false no_dangerous_types fudge add_ths
    1.38 +                   chained_ths)
    1.39        |> instantiate_inducts
    1.40           ? maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs)
    1.41        |> rearrange_facts ctxt (respect_no_atp andalso not only)