src/HOL/Tools/ATP/atp_problem_generate.ML

     Proof.context -> atp_format -> formula_kind -> formula_kind -> type_enc
     -> bool -> string -> bool -> bool -> bool -> term list -> term
     -> ((string * stature) * term) list
     -> string problem * string Symtab.table * (string * stature) list vector
        * (string * term) list * int Symtab.table
-  val atp_problem_relevance_weights : string problem -> (string * real) list
-  val atp_problem_kbo_weights : string problem -> (string * int) list
+  val atp_problem_selection_weights : string problem -> (string * real) list
+  val atp_problem_term_order_weights : string problem -> (string * int) list
 end;
 
 structure ATP_Problem_Generate : ATP_PROBLEM_GENERATE =
 struct
 

 val fact_min_weight = 0.2
 val fact_max_weight = 1.0
 val type_info_default_weight = 0.8
 
 (* Weights are from 0.0 (most important) to 1.0 (least important). *)
-fun atp_problem_relevance_weights problem =
+fun atp_problem_selection_weights problem =
   let
     fun add_term_weights weight (ATerm (s, tms)) =
         is_tptp_user_symbol s ? Symtab.default (s, weight)
         #> fold (add_term_weights weight) tms
       | add_term_weights weight (AAbs (_, tm)) = add_term_weights weight tm

       have_head_rolling (hd args) ||> append (tl args)
     else
       (s, args)
   | have_head_rolling _ = ("", [])
 
-val max_kbo_weight = 2147483647
-
-fun atp_problem_kbo_weights problem =
+val max_term_order_weight = 2147483647
+
+fun atp_problem_term_order_weights problem =
   let
     fun add_term_deps head (ATerm (s, args)) =
         is_tptp_user_symbol s ? perhaps (try (Graph.add_edge_acyclic (s, head)))
         #> fold (add_term_deps head) args
       | add_term_deps head (AAbs (_, tm)) = add_term_deps head tm

         else
           I
     val graph =
       Graph.empty |> fold (fold (add_line_deps spec_eqN) o snd) problem
                   |> fold (fold (add_line_deps simpN) o snd) problem
-    fun next_weight w = if w + w <= max_kbo_weight then w + w else w + 1
+    fun next_weight w = if w + w <= max_term_order_weight then w + w else w + 1
     fun add_weights _ [] = I
       | add_weights weight syms =
         fold (AList.update (op =) o rpair weight) syms
         #> add_weights (next_weight weight)
                (fold (union (op =) o Graph.immediate_succs graph) syms [])