src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML

 
 (** "hBOOL" and "hAPP" **)
 
 type repair_info = {pred_sym: bool, min_arity: int, max_arity: int}
 
-fun consider_combterm_for_repair explicit_apply =
+fun add_combterm_to_sym_table explicit_apply =
   let
     fun aux top_level tm =
       let val (head, args) = strip_combterm_comb tm in
         (case head of
            CombConst ((s, _), _, _) =>

          | _ => I)
         #> fold (aux false) args
       end
   in aux true end
 
-fun consider_fact_for_repair explicit_apply =
-  fact_lift (formula_fold (consider_combterm_for_repair explicit_apply))
+val add_fact_to_sym_table = fact_lift o formula_fold o add_combterm_to_sym_table
 
 (* The "equal" entry is needed for helper facts if the problem otherwise does
    not involve equality. The "$false" and $"true" entries are needed to ensure
    that no "hBOOL" is introduced for them. The "hBOOL" entry is needed to ensure
    that no "hAPP"s are introduced for passing arguments to it. *)

    (make_fixed_const boolify_base,
     {pred_sym = true, min_arity = 1, max_arity = 1})]
 
 fun sym_table_for_facts explicit_apply facts =
   Symtab.empty |> fold Symtab.default default_sym_table_entries
-               |> fold (consider_fact_for_repair explicit_apply) facts
+               |> fold (add_fact_to_sym_table explicit_apply) facts
 
 fun min_arity_of sym_tab s =
   case Symtab.lookup sym_tab s of
     SOME ({min_arity, ...} : repair_info) => min_arity
   | NONE =>

     val helper_facts =
       problem |> maps (map_filter (fn Formula (_, _, _, phi, _, _) => SOME phi
                                     | _ => NONE) o snd)
               |> get_helper_facts ctxt type_sys
               |>> map (repair_fact type_sys sym_tab)
-    val sym_tab = sym_table_for_facts explicit_apply (conjs @ facts)
+    val sym_tab = sym_table_for_facts false (conjs @ facts)
     val const_tab = const_table_for_facts type_sys sym_tab (conjs @ facts)
     val sym_decl_lines =
       Symtab.fold_rev (append o problem_lines_for_const ctxt type_sys sym_tab)
                       const_tab []
     val helper_lines =