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