1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu Apr 26 00:33:00 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu Apr 26 00:33:23 2012 +0200
     1.3 @@ -49,7 +49,8 @@
     1.4      -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list
     1.5    val all_facts :
     1.6      Proof.context -> bool -> 'a Symtab.table -> bool -> thm list
     1.7 -    -> thm list -> status Termtab.table -> (((unit -> string) * stature) * thm) list
     1.8 +    -> thm list -> status Termtab.table
     1.9 +    -> (((unit -> string) * stature) * thm) list
    1.10    val nearly_all_facts :
    1.11      Proof.context -> bool -> relevance_override -> thm list -> term list -> term
    1.12      -> (((unit -> string) * stature) * thm) list