--- 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, []) = []
--- 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