--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Nov 06 11:44:41 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Nov 06 13:36:19 2014 +0100
@@ -1467,7 +1467,8 @@
let
val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
val ctxt = ctxt |> Config.put instantiate_inducts false
- val facts = nearly_all_facts ctxt false fact_override Symtab.empty css chained [] @{prop True}
+ val facts =
+ nearly_all_facts ctxt false fact_override Keyword.empty_keywords css chained [] @{prop True}
|> sort (crude_thm_ord o pairself snd o swap)
val num_facts = length facts
val prover = hd provers