src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu May 27 17:22:16 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri May 28 13:49:21 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 chain_ths =
+fun all_valid_thms respect_no_atp ctxt chained_ths =
   let
     val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt);
     val local_facts = ProofContext.facts_of ctxt;
@@ -372,12 +372,13 @@
           val ths = filter_out bad_for_atp ths0;
         in
           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
             NONE => I
-          | SOME a => cons (a, ths)
+          | SOME name' =>
+            cons (name' |> forall (member Thm.eq_thm chained_ths) ths
+                           ? prefix chained_prefix, ths)
         end);
   in valid_facts global_facts @ valid_facts local_facts end;
 
@@ -397,10 +398,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 chain_ths =
+fun name_thm_pairs respect_no_atp ctxt chained_ths =
   let
     val (mults, singles) =
-      List.partition is_multi (all_valid_thms respect_no_atp ctxt chain_ths)
+      List.partition is_multi (all_valid_thms respect_no_atp ctxt chained_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;
@@ -409,11 +410,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 chain_ths =
+fun get_all_lemmas respect_no_atp ctxt chained_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 chain_ths)
+            (name_thm_pairs respect_no_atp ctxt chained_ths)
   in
     filter check_named included_thms
   end;
@@ -510,14 +511,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, _)) goal_cls =
+                       (ctxt, (chained_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 chain_ths
+      val included_cls = get_all_lemmas respect_no_atp ctxt chained_ths
         |> cnf_rules_pairs thy |> make_unique
         |> restrict_to_logic thy is_FO
         |> remove_unwanted_clauses
@@ -529,14 +530,8 @@
 
 (* prepare for passing to writer,
    create additional clauses based on the information from extra_cls *)
-fun prepare_clauses dfg goal_cls chain_ths axcls extra_cls thy =
+fun prepare_clauses dfg goal_cls chained_ths axcls extra_cls thy =
   let
-    (* add chain thms *)
-    val chain_cls =
-      cnf_rules_pairs thy (filter check_named
-                                  (map (`Thm.get_name_hint) chain_ths))
-    val axcls = chain_cls @ axcls
-    val extra_cls = chain_cls @ extra_cls
     val is_FO = is_first_order thy goal_cls
     val ccls = subtract_cls extra_cls goal_cls
     val _ = app (fn th => trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls