1.1 --- a/src/HOL/TPTP/mash_export.ML	Fri Jul 20 22:19:46 2012 +0200
     1.2 +++ b/src/HOL/TPTP/mash_export.ML	Fri Jul 20 22:19:46 2012 +0200
     1.3 @@ -81,11 +81,11 @@
     1.4      val facts =
     1.5        all_facts_of thy css_table
     1.6        |> not include_thy ? filter_out (has_thy thy o snd)
     1.7 -    fun do_fact ((_, (_, status)), th) =
     1.8 +    fun do_fact ((_, stature), th) =
     1.9        let
    1.10          val name = nickname_of th
    1.11          val feats =
    1.12 -          features_of ctxt prover (theory_of_thm th) status [prop_of th]
    1.13 +          features_of ctxt prover (theory_of_thm th) stature [prop_of th]
    1.14          val s = escape_meta name ^ ": " ^ escape_metas feats ^ "\n"
    1.15        in File.append path s end
    1.16    in List.app do_fact facts end
    1.17 @@ -165,10 +165,10 @@
    1.18              |>> sort (thm_ord o pairself snd)
    1.19      val ths = facts |> map snd
    1.20      val all_names = all_names ths
    1.21 -    fun do_fact ((_, (_, status)), th) prevs =
    1.22 +    fun do_fact ((_, stature), th) prevs =
    1.23        let
    1.24          val name = nickname_of th
    1.25 -        val feats = features_of ctxt prover thy status [prop_of th]
    1.26 +        val feats = features_of ctxt prover thy stature [prop_of th]
    1.27          val deps = isabelle_dependencies_of all_names th
    1.28          val kind = Thm.legacy_get_kind th
    1.29          val core = escape_metas prevs ^ "; " ^ escape_metas feats