# HG changeset patch
# User desharna
# Date 1643269944 -3600
# Node ID 16f83cea1e0aec09e2496dd4f5ae42c932a0c510
# Parent  4261983ca0cef3a55249f23c4180bc5358d9b2c6# Parent  d2f97439f53e6de39bbcd3f0f1f469f0001a21b5
merged

diff -r d2f97439f53e -r 16f83cea1e0a src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Jan 26 14:05:36 2022 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Jan 27 08:52:24 2022 +0100
@@ -391,8 +391,8 @@
 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
 
@@ -438,7 +438,7 @@
 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])
 
@@ -613,7 +613,7 @@
           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)) =
@@ -621,7 +621,7 @@
            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) =
@@ -1595,7 +1595,7 @@
     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)
@@ -1732,7 +1732,7 @@
   | 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
@@ -1740,7 +1740,7 @@
   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
 
@@ -1923,7 +1923,7 @@
 
 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
@@ -2117,7 +2117,7 @@
     (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])
@@ -2381,7 +2381,7 @@
     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, [])
@@ -2645,7 +2645,7 @@
 
         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
@@ -2688,7 +2688,7 @@
       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) =