1.1 --- a/src/HOL/TPTP/mash_eval.ML	Fri Jul 20 22:19:46 2012 +0200
     1.2 +++ b/src/HOL/TPTP/mash_eval.ML	Fri Jul 20 22:19:46 2012 +0200
     1.3 @@ -75,7 +75,7 @@
     1.4            | NONE => error ("No fact called \"" ^ name ^ "\"")
     1.5          val goal = goal_of_thm thy th
     1.6          val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
     1.7 -        val isar_deps = isabelle_dependencies_of all_names th
     1.8 +        val isar_deps = isar_dependencies_of all_names th
     1.9          val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
    1.10          val mepo_facts =
    1.11            Sledgehammer_MePo.iterative_relevant_facts ctxt params prover