1.1 --- a/src/HOL/ex/atp_export.ML	Tue Jun 21 17:17:39 2011 +0200
     1.2 +++ b/src/HOL/ex/atp_export.ML	Tue Jun 21 17:17:39 2011 +0200
     1.3 @@ -105,6 +105,14 @@
     1.4  fun ident_of_problem_line (Decl (ident, _, _)) = ident
     1.5    | ident_of_problem_line (Formula (ident, _, _, _, _)) = ident
     1.6  
     1.7 +structure String_Graph = Graph(type key = string val ord = string_ord);
     1.8 +
     1.9 +fun order_facts ord = sort (ord o pairself ident_of_problem_line)
    1.10 +fun order_problem_facts _ [] = []
    1.11 +  | order_problem_facts ord ((heading, lines) :: problem) =
    1.12 +    if heading = factsN then (heading, order_facts ord lines) :: problem
    1.13 +    else (heading, lines) :: order_problem_facts ord problem
    1.14 +
    1.15  fun generate_tptp_inference_file_for_theory ctxt thy type_sys file_name =
    1.16    let
    1.17      val format = FOF
    1.18 @@ -126,8 +134,22 @@
    1.19      val all_atp_problem_names =
    1.20        atp_problem |> maps (map ident_of_problem_line o snd)
    1.21      val infers =
    1.22 -      infers |> map (apsnd (filter (member (op =) all_atp_problem_names)))
    1.23 -    val atp_problem = atp_problem |> add_inferences_to_problem infers
    1.24 +      infers |> filter (member (op =) all_atp_problem_names o fst)
    1.25 +             |> map (apsnd (filter (member (op =) all_atp_problem_names)))
    1.26 +    val ordered_names =
    1.27 +      String_Graph.empty
    1.28 +      |> fold (String_Graph.new_node o rpair ()) all_atp_problem_names
    1.29 +      |> fold (fn (to, froms) =>
    1.30 +                  fold (fn from => String_Graph.add_edge (from, to)) froms) infers
    1.31 +      |> String_Graph.topological_order
    1.32 +    val order_tab =
    1.33 +      Symtab.empty
    1.34 +      |> fold (Symtab.insert (op =))
    1.35 +              (ordered_names ~~ (1 upto length ordered_names))
    1.36 +    val name_ord = int_ord o pairself (the o Symtab.lookup order_tab)
    1.37 +    val atp_problem =
    1.38 +      atp_problem |> add_inferences_to_problem infers
    1.39 +                  |> order_problem_facts name_ord
    1.40      val ss = tptp_lines_for_atp_problem FOF atp_problem
    1.41      val _ = app (File.append path) ss
    1.42    in () end