# HG changeset patch
# User blanchet
# Date 1297941287 -3600
# Node ID dd2125fb75f96fb600e6be35f77d794b2660e3aa
# Parent  44b2a038500139bfd968ce265427f18da7b78e86
export more functionality of Sledgehammer to applications (for experiments)

diff -r 44b2a0385001 -r dd2125fb75f9 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- 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