src/HOL/TPTP/mash_export.ML
changeset 50611 99af6b652b3a
parent 50582 001a0e12d7f1
child 50624 4d0997abce79
     1.1 --- a/src/HOL/TPTP/mash_export.ML	Fri Dec 21 14:35:29 2012 +0100
     1.2 +++ b/src/HOL/TPTP/mash_export.ML	Fri Dec 21 15:22:57 2012 +0100
     1.3 @@ -36,12 +36,6 @@
     1.4  fun in_range (from, to) j =
     1.5    j >= from andalso (to = NONE orelse j <= the to)
     1.6  
     1.7 -fun thy_map_from_facts ths =
     1.8 -  ths |> rev
     1.9 -      |> map (snd #> `(theory_of_thm #> Context.theory_name))
    1.10 -      |> AList.coalesce (op =)
    1.11 -      |> map (apsnd (map nickname_of))
    1.12 -
    1.13  fun has_thm_thy th thy =
    1.14    Context.theory_name thy = Context.theory_name (theory_of_thm th)
    1.15  
    1.16 @@ -53,18 +47,6 @@
    1.17      |> sort (thm_ord o pairself snd)
    1.18    end
    1.19  
    1.20 -fun add_thy_parent_facts thy_map thy =
    1.21 -  let
    1.22 -    fun add_last thy =
    1.23 -      case AList.lookup (op =) thy_map (Context.theory_name thy) of
    1.24 -        SOME (last_fact :: _) => insert (op =) last_fact
    1.25 -      | _ => add_parent thy
    1.26 -    and add_parent thy = fold add_last (Theory.parents_of thy)
    1.27 -  in add_parent thy end
    1.28 -
    1.29 -val thy_name_of_fact = hd o Long_Name.explode
    1.30 -fun thy_of_fact thy = Context.get_theory thy o thy_name_of_fact
    1.31 -
    1.32  fun generate_accessibility ctxt thys include_thys file_name =
    1.33    let
    1.34      val path = file_name |> Path.explode
    1.35 @@ -74,16 +56,11 @@
    1.36          val s = escape_meta fact ^ ": " ^ escape_metas prevs ^ "\n"
    1.37          val _ = File.append path s
    1.38        in [fact] end
    1.39 -    val thy_map =
    1.40 +    val facts =
    1.41        all_facts ctxt
    1.42        |> not include_thys ? filter_out (has_thys thys o snd)
    1.43 -      |> thy_map_from_facts
    1.44 -    fun do_thy facts =
    1.45 -      let
    1.46 -        val thy = thy_of_fact (Proof_Context.theory_of ctxt) (hd facts)
    1.47 -        val parents = add_thy_parent_facts thy_map thy []
    1.48 -      in fold_rev do_fact facts parents; () end
    1.49 -  in fold_rev (fn (_, facts) => fn () => do_thy facts) thy_map () end
    1.50 +      |> map (snd #> nickname_of)
    1.51 +  in fold do_fact facts []; () end
    1.52  
    1.53  fun generate_features ctxt prover thys include_thys file_name =
    1.54    let
    1.55 @@ -172,8 +149,7 @@
    1.56          in query ^ update end
    1.57        else
    1.58          ""
    1.59 -    val thy_map = old_facts |> thy_map_from_facts
    1.60 -    val parents = fold (add_thy_parent_facts thy_map) thys []
    1.61 +    val parents = map (nickname_of o snd) (the_list (try List.last old_facts))
    1.62      val new_facts = new_facts |> map (`(nickname_of o snd))
    1.63      val prevss = fst (split_last (parents :: map (single o fst) new_facts))
    1.64      val lines = Par_List.map do_fact (tag_list 1 (new_facts ~~ prevss))