--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Wed Feb 16 19:07:53 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Thu Feb 17 12:14:47 2011 +0100
@@ -41,6 +41,9 @@
val all_facts :
Proof.context -> 'a Symtab.table -> bool -> relevance_fudge -> thm list
-> thm list -> (((unit -> string) * locality) * (bool * thm)) list
+ val const_names_in_fact :
+ theory -> (string * typ -> term list -> bool * term list) -> term
+ -> string list
val relevant_facts :
Proof.context -> bool -> real * real -> int
-> (string * typ -> term list -> bool * term list) -> relevance_fudge
@@ -467,6 +470,8 @@
[] => NONE
| consts => SOME ((fact, consts), NONE)
+val const_names_in_fact = map fst ooo pconsts_in_fact
+
type annotated_thm =
(((unit -> string) * locality) * thm) * (string * ptype) list