# HG changeset patch
# User blanchet
# Date 1274102471 -7200
# Node ID 62e29faa3718a9da4d2f3ec4d97c8ed70d00349f
# Parent  3c804030474b1086a430f3cf122a2aecd768187d
make sure chained facts don't pop up in the metis proof

diff -r 3c804030474b -r 62e29faa3718 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon May 17 12:15:37 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon May 17 15:21:11 2010 +0200
@@ -352,7 +352,7 @@
 fun subtract_cls ax_clauses =
   filter_out (Termtab.defined (mk_clause_table ax_clauses) o prop_of)
 
-fun all_valid_thms respect_no_atp ctxt =
+fun all_valid_thms respect_no_atp ctxt chain_ths =
   let
     val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt);
     val local_facts = ProofContext.facts_of ctxt;
@@ -371,7 +371,8 @@
           val name2 = Name_Space.extern full_space name;
           val ths = filter_out bad_for_atp ths0;
         in
-          if Facts.is_concealed facts name orelse null ths orelse
+          if Facts.is_concealed facts name orelse
+             forall (member Thm.eq_thm chain_ths) ths orelse
              (respect_no_atp andalso is_package_def name) then
             I
           else case find_first check_thms [name1, name2, name] of
@@ -396,10 +397,10 @@
 
 (* The single-name theorems go after the multiple-name ones, so that single
    names are preferred when both are available. *)
-fun name_thm_pairs respect_no_atp ctxt =
+fun name_thm_pairs respect_no_atp ctxt chain_ths =
   let
     val (mults, singles) =
-      List.partition is_multi (all_valid_thms respect_no_atp ctxt)
+      List.partition is_multi (all_valid_thms respect_no_atp ctxt chain_ths)
     val ps = [] |> fold add_single_names singles
                 |> fold add_multi_names mults
   in ps |> respect_no_atp ? filter_out (No_ATPs.member ctxt o snd) end;
@@ -408,11 +409,11 @@
       (warning ("No name for theorem " ^ Display.string_of_thm_without_context th); false)
   | check_named _ = true;
 
-fun get_all_lemmas respect_no_atp ctxt =
+fun get_all_lemmas respect_no_atp ctxt chain_ths =
   let val included_thms =
         tap (fn ths => trace_msg
                      (fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems")))
-            (name_thm_pairs respect_no_atp ctxt)
+            (name_thm_pairs respect_no_atp ctxt chain_ths)
   in
     filter check_named included_thms
   end;
@@ -509,14 +510,14 @@
 fun get_relevant_facts respect_no_atp relevance_threshold relevance_convergence
                        defs_relevant max_new theory_relevant
                        (relevance_override as {add, only, ...})
-                       (ctxt, (chain_ths, th)) goal_cls =
+                       (ctxt, (chain_ths, _)) goal_cls =
   if (only andalso null add) orelse relevance_threshold > 1.0 then
     []
   else
     let
       val thy = ProofContext.theory_of ctxt
       val is_FO = is_first_order thy goal_cls
-      val included_cls = get_all_lemmas respect_no_atp ctxt
+      val included_cls = get_all_lemmas respect_no_atp ctxt chain_ths
         |> cnf_rules_pairs thy |> make_unique
         |> restrict_to_logic thy is_FO
         |> remove_unwanted_clauses
diff -r 3c804030474b -r 62e29faa3718 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Mon May 17 12:15:37 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Mon May 17 15:21:11 2010 +0200
@@ -582,8 +582,7 @@
       | extract_num _ = NONE
   in atp_proof |> split_lines |> map_filter (extract_num o tokens_of) end
   
-(* Used to label theorems chained into the Sledgehammer call (or rather
-   goal?) *)
+(* Used to label theorems chained into the goal. *)
 val chained_hint = "sledgehammer_chained"
 
 fun apply_command _ 1 = "by "