# HG changeset patch
# User blanchet
# Date 1297879673 -3600
# Node ID 44b2a038500139bfd968ce265427f18da7b78e86
# Parent  26dab6eca1c23119a482f7ae819969a2382951e6
export useful function (needed in a Sledgehammer-related experiment)

diff -r 26dab6eca1c2 -r 44b2a0385001 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Tue Feb 15 18:32:58 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed Feb 16 19:07:53 2011 +0100
@@ -38,6 +38,9 @@
   val fact_from_ref :
     Proof.context -> unit Symtab.table -> thm list
     -> Facts.ref * Attrib.src list -> ((string * locality) * thm) list
+  val all_facts :
+    Proof.context -> 'a Symtab.table -> bool -> relevance_fudge -> thm list
+    -> thm list -> (((unit -> string) * locality) * (bool * thm)) list
   val relevant_facts :
     Proof.context -> bool -> real * real -> int
     -> (string * typ -> term list -> bool * term list) -> relevance_fudge