--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jan 25 09:57:44 2022 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Jan 26 16:49:56 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) =