1.1 --- a/src/HOL/TPTP/atp_theory_export.ML	Mon Jul 09 23:23:12 2012 +0200
     1.2 +++ b/src/HOL/TPTP/atp_theory_export.ML	Mon Jul 09 23:23:12 2012 +0200
     1.3 @@ -129,24 +129,36 @@
     1.4      val _ = List.app (do_thy o snd) thy_ths
     1.5    in () end
     1.6  
     1.7 -(* TODO: Add types, subterms, intro/dest/elim/simp status *)
     1.8 +(* TODO: Add types, subterms *)
     1.9  fun generate_mash_feature_file_for_theory ctxt thy file_name =
    1.10    let
    1.11      val path = file_name |> Path.explode
    1.12      val _ = File.write path ""
    1.13      val axioms = Theory.all_axioms_of thy |> map fst
    1.14 -    fun do_thm th =
    1.15 +    val facts = facts_of thy
    1.16 +    fun do_fact ((_, (_, status)), th) =
    1.17        let
    1.18 +        val is_boring =
    1.19 +          String.isSubstring Sledgehammer_Filter.pseudo_skolem_prefix
    1.20          val name = Thm.get_name_hint th
    1.21          val features =
    1.22 -          (if member (op =) axioms name then ["axiom"] else []) @
    1.23            map (prefix const_prefix o escape_meta)
    1.24                (interesting_const_names ctxt (Thm.prop_of th))
    1.25 -          |> (fn [] => ["likely_tautology"] | features => features)
    1.26 +          |> (fn features =>
    1.27 +                 features |> forall is_boring features
    1.28 +                             ? cons "likely_tautology")
    1.29 +          |> (member (op =) axioms name ? cons "axiom")
    1.30 +          |> (case status of
    1.31 +                General => I
    1.32 +              | Induction => cons "induction"
    1.33 +              | Intro => cons "intro"
    1.34 +              | Inductive => cons "inductive"
    1.35 +              | Elim => cons "elim"
    1.36 +              | Simp => cons "simp"
    1.37 +              | Def => cons "def")
    1.38          val s = fact_name_of name ^ ": " ^ space_implode " " features ^ "\n"
    1.39        in File.append path s end
    1.40 -    val ths = facts_of thy |> map snd
    1.41 -    val _ = List.app do_thm ths
    1.42 +    val _ = List.app do_fact facts
    1.43    in () end
    1.44  
    1.45  fun generate_mash_dependency_file_for_theory thy file_name =