diff -r 716ec3458b1d -r d443166f9520 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Jul 26 10:48:03 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Jul 26 10:48:03 2012 +0200
@@ -29,7 +29,9 @@
     Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list
     -> (((unit -> string) * 'a) * thm) list
   val maybe_filter_no_atps : Proof.context -> ('a * thm) list -> ('a * thm) list
-  val all_facts_of : Proof.context -> status Termtab.table -> fact list
+  val all_facts :
+    Proof.context -> bool -> unit Symtab.table -> thm list -> thm list
+    -> status Termtab.table -> fact list
   val nearly_all_facts :
     Proof.context -> bool -> fact_override -> unit Symtab.table
     -> status Termtab.table -> thm list -> term list -> term -> fact list
@@ -436,10 +438,6 @@
              |> op @
   end
 
-fun all_facts_of ctxt css =
-  all_facts ctxt false Symtab.empty [] [] css
-  |> rev (* partly restore the original order of facts, for MaSh *)
-
 fun nearly_all_facts ctxt ho_atp {add, del, only} reserved css chained hyp_ts
                      concl_t =
   if only andalso null add then