1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Jul 18 08:44:04 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Jul 18 08:44:04 2012 +0200
     1.3 @@ -204,14 +204,13 @@
     1.4    andalso exists_subterm (fn Free (s, _) => s = Name.skolem Auto_Bind.thesisN
     1.5                             | _ => false) (prop_of th)
     1.6  
     1.7 -fun is_theorem_bad_for_atps ho_atp exporter thm =
     1.8 +fun is_theorem_bad_for_atps ho_atp thm =
     1.9    is_metastrange_theorem thm orelse
    1.10 -  (not exporter andalso
    1.11 -   let val t = prop_of thm in
    1.12 -     is_formula_too_complex ho_atp t orelse exists_type type_has_top_sort t orelse
    1.13 -     exists_sledgehammer_const t orelse exists_low_level_class_const t orelse
    1.14 -     is_that_fact thm
    1.15 -   end)
    1.16 +  let val t = prop_of thm in
    1.17 +    is_formula_too_complex ho_atp t orelse exists_type type_has_top_sort t orelse
    1.18 +    exists_sledgehammer_const t orelse exists_low_level_class_const t orelse
    1.19 +    is_that_fact thm
    1.20 +  end
    1.21  
    1.22  fun hackish_string_for_term ctxt t =
    1.23    Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
    1.24 @@ -346,7 +345,7 @@
    1.25  fun maybe_filter_no_atps ctxt =
    1.26    not (Config.get ctxt ignore_no_atp) ? filter_out (No_ATPs.member ctxt o snd)
    1.27  
    1.28 -fun all_facts ctxt ho_atp reserved exporter add_ths chained_ths css_table =
    1.29 +fun all_facts ctxt ho_atp reserved add_ths chained_ths css_table =
    1.30    let
    1.31      val thy = Proof_Context.theory_of ctxt
    1.32      val global_facts = Global_Theory.facts_of thy
    1.33 @@ -363,9 +362,10 @@
    1.34        Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
    1.35      fun add_facts global foldx facts =
    1.36        foldx (fn (name0, ths) =>
    1.37 -        if not exporter andalso name0 <> "" andalso
    1.38 +        if name0 <> "" andalso
    1.39             forall (not o member Thm.eq_thm_prop add_ths) ths andalso
    1.40             (Facts.is_concealed facts name0 orelse
    1.41 +            not (can (Proof_Context.get_thms ctxt) name0) orelse
    1.42              (not (Config.get ctxt ignore_no_atp) andalso
    1.43               is_package_def name0) orelse
    1.44              exists (fn s => String.isSuffix s name0)
    1.45 @@ -385,24 +385,22 @@
    1.46              #> fold (fn th => fn (j, (multis, unis)) =>
    1.47                          (j + 1,
    1.48                           if not (member Thm.eq_thm_prop add_ths th) andalso
    1.49 -                            is_theorem_bad_for_atps ho_atp exporter th then
    1.50 +                            is_theorem_bad_for_atps ho_atp th then
    1.51                             (multis, unis)
    1.52                           else
    1.53                             let
    1.54                               val new =
    1.55                                 (((fn () =>
    1.56 -                                 if name0 = "" then
    1.57 -                                   th |> backquote_thm
    1.58 -                                 else
    1.59 -                                   [Facts.extern ctxt facts name0,
    1.60 -                                    Name_Space.extern ctxt full_space name0,
    1.61 -                                    name0]
    1.62 -                                   |> find_first check_thms
    1.63 -                                   |> (fn SOME name =>
    1.64 -                                          make_name reserved multi j name
    1.65 -                                        | NONE => "")),
    1.66 -                                stature_of_thm global assms chained_ths
    1.67 -                                               css_table name0 th), th)
    1.68 +                                     if name0 = "" then
    1.69 +                                       th |> backquote_thm
    1.70 +                                     else
    1.71 +                                       [Facts.extern ctxt facts name0,
    1.72 +                                        Name_Space.extern ctxt full_space name0]
    1.73 +                                       |> find_first check_thms
    1.74 +                                       |> the_default name0
    1.75 +                                       |> make_name reserved multi j),
    1.76 +                                  stature_of_thm global assms chained_ths
    1.77 +                                                 css_table name0 th), th)
    1.78                             in
    1.79                               if multi then (new :: multis, unis)
    1.80                               else (multis, new :: unis)
    1.81 @@ -419,7 +417,7 @@
    1.82  
    1.83  fun all_facts_of thy css_table =
    1.84    let val ctxt = Proof_Context.init_global thy in
    1.85 -    all_facts ctxt false Symtab.empty true [] [] css_table
    1.86 +    all_facts ctxt false Symtab.empty [] [] css_table
    1.87      |> rev (* try to restore the original order of facts, for MaSh *)
    1.88    end
    1.89  
    1.90 @@ -438,7 +436,7 @@
    1.91                 o fact_from_ref ctxt reserved chained_ths css_table) add
    1.92         else
    1.93           let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) in
    1.94 -           all_facts ctxt ho_atp reserved false add chained_ths css_table
    1.95 +           all_facts ctxt ho_atp reserved add chained_ths css_table
    1.96             |> filter_out (member Thm.eq_thm_prop del o snd)
    1.97             |> maybe_filter_no_atps ctxt
    1.98           end)