1.1 --- a/src/HOL/TPTP/MaSh_Export.thy	Wed Jul 11 21:43:19 2012 +0200
     1.2 +++ b/src/HOL/TPTP/MaSh_Export.thy	Wed Jul 11 21:43:19 2012 +0200
     1.3 @@ -18,6 +18,11 @@
     1.4  *}
     1.5  
     1.6  ML {*
     1.7 +val do_it = true (* switch to "true" to generate the files *);
     1.8 +val thy = @{theory Nat}
     1.9 +*}
    1.10 +
    1.11 +ML {*
    1.12  if do_it then
    1.13    generate_atp_dependencies @{context} thy false "/tmp/mash_atp_dependencies"
    1.14  else
    1.15 @@ -25,11 +30,6 @@
    1.16  *}
    1.17  
    1.18  ML {*
    1.19 -val do_it = true (* switch to "true" to generate the files *);
    1.20 -val thy = @{theory Nat}
    1.21 -*}
    1.22 -
    1.23 -ML {*
    1.24  if do_it then
    1.25    generate_features thy false "/tmp/mash_features"
    1.26  else

     2.1 --- a/src/HOL/TPTP/mash_export.ML	Wed Jul 11 21:43:19 2012 +0200
     2.2 +++ b/src/HOL/TPTP/mash_export.ML	Wed Jul 11 21:43:19 2012 +0200
     2.3 @@ -201,8 +201,10 @@
     2.4          | Def => cons "def")
     2.5    end
     2.6  
     2.7 -val dependencies_of =
     2.8 -  map fact_name_of oo theorems_mentioned_in_proof_term o SOME
     2.9 +fun dependencies_of all_facts =
    2.10 +  theorems_mentioned_in_proof_term (SOME all_facts)
    2.11 +  #> map fact_name_of
    2.12 +  #> sort string_ord
    2.13  
    2.14  val freezeT = Type.legacy_freeze_type
    2.15  
    2.16 @@ -306,20 +308,30 @@
    2.17        |> not include_thy ? filter_out (has_thy thy o snd)
    2.18      val ths = facts |> map snd
    2.19      val all_names = ths |> map Thm.get_name_hint
    2.20 +    fun is_dep dep (_, th) = fact_name_of (Thm.get_name_hint th) = dep
    2.21 +    fun add_isa_dep facts dep accum =
    2.22 +      if exists (is_dep dep) accum then
    2.23 +        accum
    2.24 +      else case find_first (is_dep dep) facts of
    2.25 +        SOME ((name, status), th) => accum @ [((name (), status), th)]
    2.26 +      | NONE => accum (* shouldn't happen *)
    2.27 +    fun fix_name ((_, stature), th) =
    2.28 +      ((th |> Thm.get_name_hint |> fact_name_of, stature), th)
    2.29      fun do_thm th =
    2.30        let
    2.31          val name = Thm.get_name_hint th
    2.32          val goal = goal_of_thm th
    2.33 +        val isa_deps = dependencies_of all_names th
    2.34 +        val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
    2.35          val facts =
    2.36 -          facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
    2.37 -                |> meng_paulson_facts ctxt (the max_relevant) goal
    2.38 -                |> map (fn ((_, stature), th) =>
    2.39 -                           ((th |> Thm.get_name_hint |> fact_name_of, stature),
    2.40 -                            th))
    2.41 +          facts |> meng_paulson_facts ctxt (the max_relevant) goal
    2.42 +                |> fold (add_isa_dep facts) isa_deps
    2.43 +                |> map fix_name
    2.44          val deps =
    2.45            case run_sledgehammer ctxt facts goal of
    2.46 -            {outcome = NONE, used_facts, ...} => used_facts |> map fst
    2.47 -          | _ => dependencies_of all_names th
    2.48 +            {outcome = NONE, used_facts, ...} =>
    2.49 +            used_facts |> map fst |> sort string_ord
    2.50 +          | _ => isa_deps
    2.51          val s = fact_name_of name ^ ": " ^ space_implode " " deps ^ "\n"
    2.52        in File.append path s end
    2.53    in List.app do_thm ths end
    2.54 @@ -370,6 +382,7 @@
    2.55                val suggs =
    2.56                  old_facts |> meng_paulson_facts ctxt max_relevant goal
    2.57                            |> map (fact_name_of o fst o fst)
    2.58 +                          |> sort string_ord
    2.59                val s = fact_name_of name ^ ": " ^ space_implode " " suggs ^ "\n"
    2.60              in File.append path s end
    2.61            else