# HG changeset patch
# User blanchet
# Date 1271687628 -7200
# Node ID df47dc6c0e039de1b9e62af49e3c215e1acd785d
# Parent  8987f7a9afefa80c95c0ba8ee11556e57335eef3
got rid of somewhat pointless "pairname" function in Sledgehammer

diff -r 8987f7a9afef -r df47dc6c0e03 src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Mon Apr 19 16:33:20 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Mon Apr 19 16:33:48 2010 +0200
@@ -10,7 +10,6 @@
   val trace_msg: (unit -> string) -> unit
   val skolem_prefix: string
   val cnf_axiom: theory -> thm -> thm list
-  val pairname: thm -> string * thm
   val multi_base_blacklist: string list
   val bad_for_atp: thm -> bool
   val type_has_topsort: typ -> bool
@@ -370,7 +369,7 @@
 val update_cache = ThmCache.map o apfst o Thmtab.update;
 fun mark_seen name = ThmCache.map (apsnd (Symtab.update (name, ())));
 
-(*Exported function to convert Isabelle theorems into axiom clauses*)
+(* Convert Isabelle theorems into axiom clauses. *)
 fun cnf_axiom thy th0 =
   let val th = Thm.transfer thy th0 in
     case lookup_cache thy th of
@@ -379,11 +378,6 @@
   end;
 
 
-(**** Rules from the context ****)
-
-fun pairname th = (Thm.get_name_hint th, th);
-
-
 (**** Translate a set of theorems into CNF ****)
 
 fun pair_name_cls k (n, []) = []
diff -r 8987f7a9afef -r df47dc6c0e03 src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Mon Apr 19 16:33:20 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Mon Apr 19 16:33:48 2010 +0200
@@ -407,7 +407,7 @@
 fun count_user_clause user_lemmas (HOLClause {axiom_name, literals, ...}) =
   member (op =) user_lemmas axiom_name ? fold count_literal literals
 
-fun cnf_helper_thms thy = cnf_rules_pairs thy o map pairname
+fun cnf_helper_thms thy = cnf_rules_pairs thy o map (`Thm.get_name_hint)
 
 fun get_helper_clauses dfg thy isFO (conjectures, axcls, user_lemmas) =
   if isFO then