1.1 --- a/src/HOL/TPTP/mash_eval.ML	Wed Jul 18 08:44:03 2012 +0200
     1.2 +++ b/src/HOL/TPTP/mash_eval.ML	Wed Jul 18 08:44:03 2012 +0200
     1.3 @@ -45,7 +45,8 @@
     1.4      val prover_name = hd provers
     1.5      val path = file_name |> Path.explode
     1.6      val lines = path |> File.read_lines
     1.7 -    val facts = all_non_tautological_facts_of thy
     1.8 +    val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
     1.9 +    val facts = all_non_tautological_facts_of thy css_table
    1.10      val all_names = facts |> map (Thm.get_name_hint o snd)
    1.11      val iter_ok = Unsynchronized.ref 0
    1.12      val mash_ok = Unsynchronized.ref 0