src/HOL/Tools/ATP/atp_problem_generate.ML

     fun ary (Type (@{type_name fun}, [_, T])) = 1 + ary T
       | ary _ = 0
   in ary oo robust_const_type end
 
 (* This function only makes sense if "T" is as general as possible. *)
-fun robust_const_typargs thy (s, T) =
+fun robust_const_type_args thy (s, T) =
   if s = app_op_name then
     let val (T1, T2) = T |> domain_type |> dest_funT in [T1, T2] end
   else if String.isPrefix old_skolem_const_prefix s then
     [] |> Term.add_tvarsT T |> rev |> map TVar
   else if String.isPrefix lam_lifted_prefix s then

       val (P', P_atomics_Ts) = iterm_from_term thy type_enc bs P
       val (Q', Q_atomics_Ts) = iterm_from_term thy type_enc bs Q
     in (IApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
   | iterm_from_term thy type_enc _ (Const (c, T)) =
     (IConst (`(make_fixed_const (SOME type_enc)) c, T,
-             robust_const_typargs thy (c, T)),
+             robust_const_type_args thy (c, T)),
      atomic_types_of T)
   | iterm_from_term _ _ _ (Free (s, T)) =
     (IConst (`make_fixed_var s, T, []), atomic_types_of T)
   | iterm_from_term _ type_enc _ (Var (v as (s, _), T)) =
     (if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then

                 if keep (member (op =) in_U_vars U_var,
                          member (op =) out_U_vars U_var) then
                   T
                 else
                   dummyT
-              val U_args = (s, U) |> robust_const_typargs thy
+              val U_args = (s, U) |> robust_const_type_args thy
             in map (filt o apfst dest_TVar) (U_args ~~ T_args) end
             handle TYPE _ => T_args
         val noninfer_type_args = gen_type_args (not o fst) (chop_fun ary)
         val constr_infer_type_args = gen_type_args fst strip_type
         val level = level_of_type_enc type_enc

                                                 quote s)) parse_mangled_type))
     |> fst
 
 fun unmangled_const_name s =
   (s, s) |> unaliased_uncurried |> fst |> space_explode mangled_type_sep
+
 fun unmangled_const s =
   let val ss = unmangled_const_name s in
     (hd ss, map unmangled_type (tl ss))
   end
+
+val unmangled_invert_const = invert_const o hd o unmangled_const_name
 
 fun introduce_proxies_in_iterm type_enc =
   let
     fun tweak_ho_quant ho_quant T [IAbs _] = IConst (`I ho_quant, T, [])
       | tweak_ho_quant ho_quant (T as Type (_, [p_T as Type (_, [x_T, _]), _]))

     case unprefix_and_unascii const_prefix s of
       NONE =>
       if level_of_type_enc type_enc = No_Types orelse s = tptp_choice then []
       else T_args
     | SOME s'' =>
-      filter_type_args thy constrs type_enc (invert_const s'') ary T_args
+      filter_type_args thy constrs type_enc (unmangled_invert_const s'') ary T_args
 fun filter_type_args_in_iterm thy constrs type_enc =
   let
     fun filt ary (IApp (tm1, tm2)) = IApp (filt (ary + 1) tm1, filt 0 tm2)
       | filt ary (IConst (name as (s, _), T, T_args)) =
         filter_type_args_in_const thy constrs type_enc ary s T_args

 
 fun tvar_footprint thy s ary =
   (case unprefix_and_unascii const_prefix s of
      SOME s =>
      let fun tvars_of T = [] |> Term.add_tvarsT T |> map fst in
-       s |> invert_const |> robust_const_type thy |> chop_fun ary |> fst
-         |> map tvars_of
+       s |> unmangled_invert_const |> robust_const_type thy |> chop_fun ary
+         |> fst |> map tvars_of
      end
    | NONE => [])
   handle TYPE _ => []
 
 fun type_arg_cover thy pos s ary =

                       case unprefix_and_unascii const_prefix s of
                         SOME s =>
                         (if String.isSubstring uncurried_alias_sep s then
                            ary
                          else case try (robust_const_ary thy
-                                        o invert_const o hd
-                                        o unmangled_const_name) s of
+                                        o unmangled_invert_const) s of
                            SOME ary0 => Int.min (ary0, ary)
                          | NONE => ary)
                       | NONE => ary
                     val min_ary =
                       case app_op_level of

   case Symtab.lookup sym_tab s of
     SOME ({min_ary, ...} : sym_info) => min_ary
   | NONE =>
     case unprefix_and_unascii const_prefix s of
       SOME s =>
-      let val s = s |> unmangled_const_name |> hd |> invert_const in
+      let val s = s |> unmangled_invert_const in
         if s = predicator_name then 1
         else if s = app_op_name then 2
         else if s = type_guard_name then 1
         else 0
       end

 fun add_type_constrs_in_term thy =
   let
     fun add (Const (@{const_name Meson.skolem}, _) $ _) = I
       | add (t $ u) = add t #> add u
       | add (Const x) =
-        x |> robust_const_typargs thy |> fold (fold_type_constrs set_insert)
+        x |> robust_const_type_args thy |> fold (fold_type_constrs set_insert)
       | add (Abs (_, _, u)) = add u
       | add _ = I
   in add end
 
 fun type_constrs_of_terms thy ts =

       if null T_args then
         (T, [])
       else case unprefix_and_unascii const_prefix s of
         SOME s' =>
         let
-          val s' = s' |> invert_const
+          val s' = s' |> unmangled_invert_const
           val T = s' |> robust_const_type thy
-        in (T, robust_const_typargs thy (s', T)) end
+        in (T, robust_const_type_args thy (s', T)) end
       | NONE => raise Fail "unexpected type arguments"
   in
     Sym_Decl (sym_decl_prefix ^ s, (s, s'),
               T |> fused_type ctxt mono (level_of_type_enc type_enc) ary
                 |> native_ho_type_from_typ type_enc pred_sym ary

       let
         val thy = Proof_Context.theory_of ctxt
         val (role, maybe_negate) = honor_conj_sym_role in_conj
         val base_name = base_s0 |> `(make_fixed_const (SOME type_enc))
         val T = case types of [T] => T | _ => robust_const_type thy base_s0
-        val T_args = robust_const_typargs thy (base_s0, T)
+        val T_args = robust_const_type_args thy (base_s0, T)
         val (base_name as (base_s, _), T_args) =
           mangle_type_args_in_const type_enc base_name T_args
         val base_ary = min_ary_of sym_tab0 base_s
         fun do_const name = IConst (name, T, T_args)
         val filter_ty_args = filter_type_args_in_iterm thy constrs type_enc

         sym_tab (s, {min_ary, types, in_conj, ...} : sym_info) =
   case unprefix_and_unascii const_prefix s of
     SOME mangled_s =>
     if String.isSubstring uncurried_alias_sep mangled_s then
       let
-        val base_s0 = mangled_s |> unmangled_const_name |> hd |> invert_const
+        val base_s0 = mangled_s |> unmangled_invert_const
       in
         do_uncurried_alias_lines_for_sym ctxt constrs mono type_enc sym_tab0
                                          sym_tab base_s0 types in_conj min_ary
       end
     else