diff -r 480746f1012c -r ca998fa08cd9 src/HOL/TPTP/mash_export.ML
--- a/src/HOL/TPTP/mash_export.ML	Fri Jul 20 22:19:46 2012 +0200
+++ b/src/HOL/TPTP/mash_export.ML	Fri Jul 20 22:19:46 2012 +0200
@@ -102,13 +102,13 @@
     fun do_thm th =
       let
         val name = nickname_of th
-        val deps = isabelle_dependencies_of all_names th
+        val deps = isar_dependencies_of all_names th
         val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n"
       in File.append path s end
   in List.app do_thm ths end
 
-fun generate_atp_dependencies ctxt (params as {provers, max_facts, ...}) thy
-                              include_thy file_name =
+fun generate_atp_dependencies ctxt (params as {provers, ...}) thy include_thy
+                              file_name =
   let
     val path = file_name |> Path.explode
     val _ = File.write path ""
@@ -118,38 +118,11 @@
       |> not include_thy ? filter_out (has_thy thy o snd)
     val ths = facts |> map snd
     val all_names = all_names ths
-    fun is_dep dep (_, th) = nickname_of th = dep
-    fun add_isar_dep facts dep accum =
-      if exists (is_dep dep) accum then
-        accum
-      else case find_first (is_dep dep) facts of
-        SOME ((name, status), th) => accum @ [((name, status), th)]
-      | NONE => accum (* shouldn't happen *)
-    fun fix_name ((_, stature), th) = ((fn () => nickname_of th, stature), th)
     fun do_thm th =
       let
         val name = nickname_of th
-        val goal = goal_of_thm thy th
-        val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
         val deps =
-          case isabelle_dependencies_of all_names th of
-            [] => []
-          | isar_dep as [_] => isar_dep (* can hardly beat that *)
-          | isar_deps =>
-            let
-              val facts =
-                facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
-              val facts =
-                facts |> iterative_relevant_facts ctxt params prover
-                             (the max_facts) NONE hyp_ts concl_t
-                      |> fold (add_isar_dep facts) isar_deps
-                      |> map fix_name
-            in
-              case run_prover_for_mash ctxt params prover facts goal of
-                {outcome = NONE, used_facts, ...} =>
-                used_facts |> map fst |> sort string_ord
-              | _ => isar_deps
-            end
+          atp_dependencies_of ctxt params prover false facts all_names th
         val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n"
       in File.append path s end
   in List.app do_thm ths end
@@ -169,7 +142,7 @@
       let
         val name = nickname_of th
         val feats = features_of ctxt prover thy stature [prop_of th]
-        val deps = isabelle_dependencies_of all_names th
+        val deps = isar_dependencies_of all_names th
         val kind = Thm.legacy_get_kind th
         val core = escape_metas prevs ^ "; " ^ escape_metas feats
         val query = if kind <> "" then "? " ^ core ^ "\n" else ""
@@ -207,7 +180,6 @@
                 |> Sledgehammer_MePo.iterative_relevant_facts ctxt params prover
                        max_relevant NONE hyp_ts concl_t
                 |> map (fn ((name, _), _) => name ())
-                |> sort string_ord
               val s = escape_meta name ^ ": " ^ escape_metas suggs ^ "\n"
             in File.append path s end
           else