src/HOL/Tools/ATP/atp_problem_generate.ML

 fun make_tvar (s, i) = tvar_prefix ^ ascii_of_indexname (unquote_tvar s, i)
 fun make_tfree s = tfree_prefix ^ ascii_of (unquote_tvar s)
 fun tvar_name ((x as (s, _)), _) = (make_tvar x, s)
 
 (* "HOL.eq" and choice are mapped to the ATP's equivalents *)
-fun make_fixed_const _ \<^const_name>\<open>HOL.eq\<close> = tptp_old_equal
-  | make_fixed_const _ c = const_prefix ^ lookup_const c
+fun make_fixed_const \<^const_name>\<open>HOL.eq\<close> = tptp_old_equal
+  | make_fixed_const c = const_prefix ^ lookup_const c
 
 fun make_fixed_type_const c = type_const_prefix ^ lookup_const c
 
 fun make_class clas = class_prefix ^ ascii_of clas
 

 val tvar_a_str = "'a"
 val tvar_a_z = ((tvar_a_str, 0), \<^sort>\<open>type\<close>)
 val tvar_a = TVar tvar_a_z
 val tvar_a_name = tvar_name tvar_a_z
 val itself_name = `make_fixed_type_const \<^type_name>\<open>itself\<close>
-val TYPE_name = `(make_fixed_const NONE) \<^const_name>\<open>Pure.type\<close>
+val TYPE_name = `make_fixed_const \<^const_name>\<open>Pure.type\<close>
 val tvar_a_atype = AType ((tvar_a_name, []), [])
 val a_itself_atype = AType ((itself_name, []), [tvar_a_atype])
 
 (** Definitions and functions for FOL clauses and formulas for TPTP **)
 

         let
           val (P', P_atomics_Ts) = iot fool bs P
           val (Q', Q_atomics_Ts) = iot fool bs Q
         in (IApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
       | iot _ _ (Const (c, T)) =
-        (IConst (`(make_fixed_const (SOME type_enc)) c, T, robust_const_type_args thy (c, T)),
+        (IConst (`make_fixed_const c, T, robust_const_type_args thy (c, T)),
          atomic_types_of T)
       | iot _ _ (Free (s, T)) = (IConst (`make_fixed_var s, T, []), atomic_types_of T)
       | iot _ _ (Var (v as (s, _), T)) =
         (if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
            let
              val Ts = T |> strip_type |> swap |> op ::
              val s' = new_skolem_const_name s (length Ts)
-           in IConst (`(make_fixed_const (SOME type_enc)) s', T, Ts) end
+           in IConst (`make_fixed_const s', T, Ts) end
          else
            IVar ((make_schematic_var v, s), T), atomic_types_of T)
       | iot _ bs (Bound j) =
         nth bs j |> (fn (_, (name, T)) => (IConst (name, T, []), atomic_types_of T))
       | iot fool bs (Abs (s, T, t)) =

 fun default_sym_tab_entries type_enc =
   let
     fun mk_sym_info pred n =
       {pred_sym = pred, min_ary = n, max_ary = n, types = [], in_conj = false}
   in
-    (make_fixed_const NONE \<^const_name>\<open>undefined\<close>, mk_sym_info false 0) ::
+    (make_fixed_const \<^const_name>\<open>undefined\<close>, mk_sym_info false 0) ::
     (map (apsnd (fn {arity, is_predicate} => mk_sym_info is_predicate arity))
       (Symtab.dest tptp_builtins))
     |> not (is_type_enc_fool type_enc orelse is_type_enc_full_higher_order type_enc)
       ? cons (prefixed_predicator_name, mk_sym_info true 1)
   end

   (case Symtab.lookup sym_tab s of
     SOME ({pred_sym, min_ary, max_ary, ...} : sym_info) => pred_sym andalso min_ary = max_ary
   | NONE => false)
 
 val fTrue_iconst = IConst ((const_prefix ^ "fTrue", \<^const_name>\<open>fTrue\<close>), \<^typ>\<open>bool\<close>, [])
-val predicator_iconst = IConst (`(make_fixed_const NONE) predicator_name, \<^typ>\<open>bool => bool\<close>, [])
+val predicator_iconst = IConst (`make_fixed_const predicator_name, \<^typ>\<open>bool => bool\<close>, [])
 
 fun predicatify completish tm =
   if completish > 1 then
     IApp (IApp (IConst (`I tptp_equal, \<^typ>\<open>bool => bool => bool\<close>, []), tm), fTrue_iconst)
   else
     IApp (predicator_iconst, tm)
 
-val app_op = `(make_fixed_const NONE) app_op_name
+val app_op = `make_fixed_const app_op_name
 
 fun list_app head args = fold (curry (IApp o swap)) args head
 
 fun mk_app_op type_enc head arg =
   let

 val min_rank = 9 * helper_rank div 10
 val max_rank = 4 * min_rank
 
 fun rank_of_fact_num n j = min_rank + (max_rank - min_rank) * j div n
 
-val type_tag = `(make_fixed_const NONE) type_tag_name
+val type_tag = `make_fixed_const type_tag_name
 
 fun could_specialize_helpers type_enc =
   not (is_type_enc_polymorphic type_enc) andalso level_of_type_enc type_enc <> No_Types
 
 fun should_specialize_helper type_enc t =

     val subclass_pairs = make_subclass_pairs thy subs supers
   in
     (union (op =) subs supers, conjs, facts @ lam_facts, subclass_pairs, tcon_clauses, lifted)
   end
 
-val type_guard = `(make_fixed_const NONE) type_guard_name
+val type_guard = `make_fixed_const type_guard_name
 
 fun type_guard_iterm type_enc T tm =
   IApp (IConst (type_guard, T --> \<^typ>\<open>bool\<close>, [T])
         |> mangle_type_args_in_iterm type_enc, tm)
 

        and this declaration causes problems in FOF if undefined_bool occurs without predicator pp.
      *)
     fun add_undefined_const \<^Type>\<open>bool\<close> = I
       | add_undefined_const T =
         let
-          val name = `(make_fixed_const NONE) \<^const_name>\<open>undefined\<close>
+          val name = `make_fixed_const \<^const_name>\<open>undefined\<close>
           val ((s, s'), Ts) =
             if is_type_enc_mangling type_enc then
               (mangled_const_name type_enc [T] name, [])
             else
               (name, [T])

       let
         val thy = Proof_Context.theory_of ctxt
 
         fun do_ctr (s, T) =
           let
-            val s' = make_fixed_const (SOME type_enc) s
+            val s' = make_fixed_const s
             val ary = ary_of T
             fun mk name = SOME (mk_aterm type_enc name (robust_const_type_args thy (s, T)) [])
           in
             if T = HOLogic.boolT then
               (case proxify_const s' of

   let
     fun do_alias 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 base_name = base_s0 |> `make_fixed_const
         val T = (case types of [T] => T | _ => robust_const_type thy base_s0)
         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