# HG changeset patch
# User blanchet
# Date 1271687600 -7200
# Node ID 8987f7a9afefa80c95c0ba8ee11556e57335eef3
# Parent  ed7306094efe36e9bcfb739db1a2a157a8a727ac
make Sledgehammer's "add:" and "del:" syntax really work (I hope), by comparing CNF theorems with CNF theorems

diff -r ed7306094efe -r 8987f7a9afef src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Apr 19 16:29:52 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Apr 19 16:33:20 2010 +0200
@@ -254,8 +254,10 @@
 fun relevant_clauses ctxt convergence follow_defs max_new
                      (relevance_override as {add, del, only}) thy ctab =
   let
-    val add_thms = maps (ProofContext.get_fact ctxt) add
-    val del_thms = maps (ProofContext.get_fact ctxt) del
+    val thms_for_facts =
+      maps (maps (cnf_axiom thy) o ProofContext.get_fact ctxt)
+    val add_thms = thms_for_facts add
+    val del_thms = thms_for_facts del
     fun iter p rel_consts =
       let
         fun relevant ([], _) [] = []  (* Nothing added this iteration *)
@@ -366,11 +368,11 @@
           val ths = filter_out bad_for_atp ths0;
         in
           if Facts.is_concealed facts name orelse null 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))
+             (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)
         end);
   in valid_facts global_facts @ valid_facts local_facts end;
 
@@ -528,7 +530,8 @@
   let
     (* add chain thms *)
     val chain_cls =
-      cnf_rules_pairs thy (filter check_named (map pairname chain_ths))
+      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 higher_order goal_cls