1.1 --- a/src/HOL/TPTP/mash_eval.ML	Thu Jul 26 10:48:03 2012 +0200
     1.2 +++ b/src/HOL/TPTP/mash_eval.ML	Thu Jul 26 10:48:03 2012 +0200
     1.3 @@ -36,8 +36,9 @@
     1.4      val slack_max_facts = max_facts_slack * the max_facts
     1.5      val path = file_name |> Path.explode
     1.6      val lines = path |> File.read_lines
     1.7 -    val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
     1.8 -    val facts = all_facts_of (Proof_Context.init_global thy) css_table
     1.9 +    val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
    1.10 +    val facts =
    1.11 +      all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css
    1.12      val all_names = all_names (facts |> map snd)
    1.13      val mepo_ok = Unsynchronized.ref 0
    1.14      val mash_ok = Unsynchronized.ref 0
    1.15 @@ -70,7 +71,7 @@
    1.16          val th =
    1.17            case find_first (fn (_, th) => nickname_of th = name) facts of
    1.18              SOME (_, th) => th
    1.19 -          | NONE => error ("No fact called \"" ^ name ^ "\"")
    1.20 +          | NONE => error ("No fact called \"" ^ name ^ "\".")
    1.21          val goal = goal_of_thm thy th
    1.22          val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
    1.23          val isar_deps = isar_dependencies_of all_names th |> these