--- a/src/Doc/Eisbach/Base.thy Sun Aug 04 16:56:28 2024 +0200
+++ b/src/Doc/Eisbach/Base.thy Sun Aug 04 17:39:47 2024 +0200
@@ -12,7 +12,7 @@
fun get_split_rule ctxt target =
let
val (head, args) = strip_comb (Envir.eta_contract target);
- val (const_name, _) = dest_Const head;
+ val const_name = dest_Const_name head;
val const_name_components = Long_Name.explode const_name;
val _ =
--- a/src/HOL/Data_Structures/Define_Time_Function.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Data_Structures/Define_Time_Function.ML Sun Aug 04 17:39:47 2024 +0200
@@ -543,9 +543,9 @@
(* Print result if print *)
val _ = if not print then () else
let
- val nms = map (fst o dest_Const) term
+ val nms = map dest_Const_name term
val used = map (used_for_const orig_used) term
- val typs = map (snd o dest_Const) term
+ val typs = map dest_Const_type term
in
print_timing' print_ctxt { names=nms, terms=terms, typs=typs } { names=timing_names, terms=T_terms, typs=map (fn (used, typ) => change_typ' used 0 typ) (zip used typs) }
end
@@ -610,8 +610,8 @@
(* Print result if print *)
val _ = if not print then () else
let
- val nms = map (fst o dest_Const) term
- val typs = map (snd o dest_Const) term
+ val nms = map dest_Const_name term
+ val typs = map dest_Const_type term
in
print_timing' print_ctxt { names=nms, terms=terms, typs=typs } (info_pfunc time_info)
end
--- a/src/HOL/Decision_Procs/Conversions.thy Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Decision_Procs/Conversions.thy Sun Aug 04 17:39:47 2024 +0200
@@ -24,7 +24,7 @@
\<open>convert equality to meta equality\<close>
ML \<open>
-fun strip_app ct = ct |> Drule.strip_comb |>> Thm.term_of |>> dest_Const |>> fst;
+fun strip_app ct = ct |> Drule.strip_comb |>> Thm.term_of |>> dest_Const_name;
fun inst cTs cts th =
Thm.instantiate' (map SOME cTs) (map SOME cts) th;
--- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Sun Aug 04 17:39:47 2024 +0200
@@ -446,8 +446,8 @@
(* define syntax for case combinator *)
(* TODO: re-implement case syntax using a parse translation *)
local
- fun syntax c = Lexicon.mark_const (fst (dest_Const c))
- fun xconst c = Long_Name.base_name (fst (dest_Const c))
+ fun syntax c = Lexicon.mark_const (dest_Const_name c)
+ fun xconst c = Long_Name.base_name (dest_Const_name c)
fun c_ast authentic con = Ast.Constant (if authentic then syntax con else xconst con)
fun showint n = string_of_int (n+1)
fun expvar n = Ast.Variable ("e" ^ showint n)
@@ -803,8 +803,8 @@
(* register match combinators with fixrec package *)
local
- val con_names = map (fst o dest_Const o fst) spec
- val mat_names = map (fst o dest_Const) match_consts
+ val con_names = map (dest_Const_name o fst) spec
+ val mat_names = map dest_Const_name match_consts
in
val thy = Fixrec.add_matchers (con_names ~~ mat_names) thy
end
--- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Sun Aug 04 17:39:47 2024 +0200
@@ -223,7 +223,7 @@
if length dnames = 1 then ["bottom"] else
map (fn s => "bottom_" ^ Long_Name.base_name s) dnames
fun one_eq bot (constr_info : Domain_Constructors.constr_info) =
- let fun name_of (c, _) = Long_Name.base_name (fst (dest_Const c))
+ let fun name_of (c, _) = Long_Name.base_name (dest_Const_name c)
in bot :: map name_of (#con_specs constr_info) end
in adms @ flat (map2 one_eq bottoms constr_infos) end
--- a/src/HOL/HOLCF/Tools/fixrec.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/HOLCF/Tools/fixrec.ML Sun Aug 04 17:39:47 2024 +0200
@@ -293,8 +293,7 @@
val concl = HOLogic.dest_Trueprop o Logic.strip_imp_concl o strip_alls
fun tac (t, i) =
let
- val (c, _) =
- (dest_Const o head_of o chead_of o fst o HOLogic.dest_eq o concl) t
+ val c = dest_Const_name (head_of (chead_of (fst (HOLogic.dest_eq (concl t)))))
val unfold_thm = the (Symtab.lookup tab c)
val rule = unfold_thm RS @{thm ssubst_lhs}
in
--- a/src/HOL/HOLCF/ex/Pattern_Match.thy Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/HOLCF/ex/Pattern_Match.thy Sun Aug 04 17:39:47 2024 +0200
@@ -494,7 +494,7 @@
(* syntax translations for pattern combinators *)
local
- fun syntax c = Lexicon.mark_const (fst (dest_Const c));
+ fun syntax c = Lexicon.mark_const (dest_Const_name c);
fun app s (l, r) = Ast.mk_appl (Ast.Constant s) [l, r];
val capp = app \<^const_syntax>\<open>Rep_cfun\<close>;
val capps = Library.foldl capp
--- a/src/HOL/Hoare/hoare_syntax.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Hoare/hoare_syntax.ML Sun Aug 04 17:39:47 2024 +0200
@@ -199,10 +199,10 @@
fun com_tr' ctxt (t,a) =
let
- val (head, args) = apfst (try (#1 o Term.dest_Const)) (Term.strip_comb t);
+ val (head, args) = apfst (try Term.dest_Const_name) (Term.strip_comb t);
fun arg k = nth args (k - 1);
val n = length args;
- val (_, args_a) = apfst (try (#1 o Term.dest_Const)) (Term.strip_comb a);
+ val (_, args_a) = apfst (try Term.dest_Const_name) (Term.strip_comb a);
fun arg_a k = nth args_a (k - 1)
in
case head of
--- a/src/HOL/Import/import_data.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Import/import_data.ML Sun Aug 04 17:39:47 2024 +0200
@@ -71,8 +71,7 @@
let
val th = Thm.legacy_freezeT th
val name = case name_opt of
- NONE => (fst o dest_Const o fst o HOLogic.dest_eq o
- HOLogic.dest_Trueprop o Thm.prop_of) th
+ NONE => dest_Const_name (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of th))))
| SOME n => n
val thy' = add_const_map s name thy
in
@@ -87,8 +86,8 @@
val (l, _) = dest_comb (HOLogic.dest_Trueprop (Thm.prop_of th))
val (l, abst) = dest_comb l
val (_, rept) = dest_comb l
- val (absn, _) = dest_Const abst
- val (repn, _) = dest_Const rept
+ val absn = dest_Const_name abst
+ val repn = dest_Const_name rept
val nty = domain_type (fastype_of rept)
val ntyn = dest_Type_name nty
val thy2 = add_typ_map tyname ntyn thy
--- a/src/HOL/Library/Tools/smt_word.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Library/Tools/smt_word.ML Sun Aug 04 17:39:47 2024 +0200
@@ -63,7 +63,7 @@
fun if_fixed_args m = if_fixed (forall (can dest_wordT) o snd) m
fun add_word_fun f (t, n) =
- let val (m, _) = Term.dest_Const t
+ let val m = dest_Const_name t
in SMT_Builtin.add_builtin_fun smtlibC (Term.dest_Const t, K (f m n)) end
val mk_nat = HOLogic.mk_number \<^typ>\<open>nat\<close>
--- a/src/HOL/Library/adhoc_overloading.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Library/adhoc_overloading.ML Sun Aug 04 17:39:47 2024 +0200
@@ -222,7 +222,7 @@
fun adhoc_overloading_cmd add raw_args lthy =
let
fun const_name ctxt =
- fst o dest_Const o Proof_Context.read_const {proper = false, strict = false} ctxt; (* FIXME {proper = true, strict = true} (!?) *)
+ dest_Const_name o Proof_Context.read_const {proper = false, strict = false} ctxt; (* FIXME {proper = true, strict = true} (!?) *)
fun read_term ctxt = singleton (Variable.polymorphic ctxt) o Syntax.read_term ctxt;
val args =
raw_args
--- a/src/HOL/Library/case_converter.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Library/case_converter.ML Sun Aug 04 17:39:47 2024 +0200
@@ -121,7 +121,7 @@
val coords = map_filter I (map_index recurse patss)
in
if null coords then NONE
- else SOME (Coordinate (map (pair (dest_Const f |> fst)) coords))
+ else SOME (Coordinate (map (pair (dest_Const_name f)) coords))
end
else SOME (End (body_type (fastype_of f)))
end
@@ -133,8 +133,7 @@
(* AL: TODO: change from term to const_name *)
fun find_ctr ctr1 xs =
let
- val const_name = fst o dest_Const
- fun const_equal (ctr1, ctr2) = const_name ctr1 = const_name ctr2
+ fun const_equal (ctr1, ctr2) = dest_Const_name ctr1 = dest_Const_name ctr2
in
lookup_remove const_equal ctr1 xs
end;
@@ -190,7 +189,7 @@
val (ctr, args) = strip_comb term
fun map_ctr (term, pat) =
let
- val args = term |> dest_Const |> snd |> binder_types |> map (fn T => Free ("x", T))
+ val args = term |> dest_Const_type |> binder_types |> map (fn T => Free ("x", T))
in
pattern_lookup args pat
end
@@ -347,7 +346,7 @@
let
fun abort t =
let
- val fun_name = head_of t |> dest_Const |> fst
+ val fun_name = dest_Const_name (head_of t)
val msg = "Missing pattern in " ^ fun_name ^ "."
in
mk_abort msg t
--- a/src/HOL/Library/code_lazy.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Library/code_lazy.ML Sun Aug 04 17:39:47 2024 +0200
@@ -279,7 +279,7 @@
val (caseT', lthy') = substitute_ctr (to_destr_eagerT caseT, eagerT) caseT lthy3
in (Const (eager_case, caseT'), lthy') end
- val ctr_names = map (Long_Name.base_name o fst o dest_Const) ctrs
+ val ctr_names = map (Long_Name.base_name o dest_Const_name) ctrs
val ((((lazy_ctr_name, lazy_sel_name), lazy_ctrs_name), lazy_case_name), ctxt) = lthy4
|> mk_name "Lazy_" "" short_type_name
||>> mk_name "unlazy_" "" short_type_name
@@ -320,7 +320,7 @@
fun mk_lazy_ctr (name, eager_ctr) =
let
- val (_, ctrT) = dest_Const eager_ctr
+ val ctrT = dest_Const_type eager_ctr
fun to_lazy_ctrT (Type (\<^type_name>\<open>fun\<close>, [T1, T2])) = T1 --> to_lazy_ctrT T2
| to_lazy_ctrT T = if T = eagerT then lazy_type else raise Match
val lazy_ctrT = to_lazy_ctrT ctrT
@@ -334,7 +334,7 @@
val (lazy_case_def, lthy8) =
let
- val (_, caseT) = dest_Const case'
+ val caseT = dest_Const_type case'
fun to_lazy_caseT (Type (\<^type_name>\<open>fun\<close>, [T1, T2])) =
if T1 = eagerT then lazy_type --> T2 else T1 --> to_lazy_caseT T2
val lazy_caseT = to_lazy_caseT caseT
@@ -385,7 +385,7 @@
fun mk_lazy_ctr_eq (eager_ctr, lazy_ctr) =
let
- val (_, ctrT) = dest_Const eager_ctr
+ val ctrT = dest_Const_type eager_ctr
val argsT = binder_types ctrT
val args = length argsT
in
@@ -401,7 +401,7 @@
fun mk_ctrs_lazy_eq (eager_ctr, lazy_ctr) =
let
- val argsT = dest_Const eager_ctr |> snd |> binder_types
+ val argsT = binder_types (dest_Const_type eager_ctr)
val n = length argsT
val lhs = apply_bounds 0 n eager_ctr
val rhs = #const lazy_ctr_def $
@@ -423,7 +423,7 @@
val case_lazy_eq =
let
- val (_, caseT) = case' |> dest_Const
+ val caseT = dest_Const_type case'
val argsT = binder_types caseT
val n = length argsT
val lhs = apply_bounds 0 n case'
@@ -447,10 +447,10 @@
fun mk_case_ctrs_eq (i, lazy_ctr) =
let
val lazy_case = #const lazy_case_def
- val (_, ctrT) = dest_Const lazy_ctr
+ val ctrT = dest_Const_type lazy_ctr
val ctr_argsT = binder_types ctrT
val ctr_args_n = length ctr_argsT
- val (_, caseT) = dest_Const lazy_case
+ val caseT = dest_Const_type lazy_case
val case_argsT = binder_types caseT
fun n_bounds_from m n t =
@@ -537,7 +537,7 @@
val table = Laziness_Data.get thy
in fn (s1, s2) => case Symtab.lookup table s1 of
NONE => false
- | SOME x => #active x andalso s2 <> (#ctr x |> dest_Const |> fst)
+ | SOME x => #active x andalso s2 <> dest_Const_name (#ctr x)
end
val thy = Proof_Context.theory_of ctxt
val table = Laziness_Data.get thy
@@ -577,7 +577,7 @@
val ctxt = Proof_Context.init_global thy
fun pretty_ctr ctr =
let
- val argsT = dest_Const ctr |> snd |> binder_types
+ val argsT = binder_types (dest_Const_type ctr)
in
Pretty.block [
Syntax.pretty_term ctxt ctr,
--- a/src/HOL/Library/conditional_parametricity.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Library/conditional_parametricity.ML Sun Aug 04 17:39:47 2024 +0200
@@ -57,7 +57,7 @@
fun strip_prop_safe t = Logic.unprotect t handle TERM _ => t;
fun get_class_of ctxt t =
- Axclass.class_of_param (Proof_Context.theory_of ctxt) (fst (dest_Const t));
+ Axclass.class_of_param (Proof_Context.theory_of ctxt) (dest_Const_name t);
fun is_class_op ctxt t =
let
@@ -347,7 +347,7 @@
val prop = Thm.prop_of thm
val (t, mk_prop') = dest prop
val Domainp_ts = rev (fold_Domainp (fn t => insert op= t) t [])
- val Domainp_Ts = map (snd o dest_funT o snd o dest_Const o fst o dest_comb) Domainp_ts
+ val Domainp_Ts = map (snd o dest_funT o dest_Const_type o fst o dest_comb) Domainp_ts
val used = Term.add_free_names t []
val rels = map (snd o dest_comb) Domainp_ts
val rel_names = map (fst o fst o dest_Var) rels
@@ -404,7 +404,7 @@
| is_eq _ = false
val add_eqs = Term.fold_aterms (fn t => if is_eq t then insert (op =) t else I)
val eq_consts = rev (add_eqs t [])
- val eqTs = map (snd o dest_Const) eq_consts
+ val eqTs = map dest_Const_type eq_consts
val used = Term.add_free_names prop []
val names = map (K "") eqTs |> Name.variant_list used
val frees = map Free (names ~~ eqTs)
--- a/src/HOL/Library/datatype_records.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Library/datatype_records.ML Sun Aug 04 17:39:47 2024 +0200
@@ -55,7 +55,7 @@
val simp_thms = flat sel_thmss @ injects
fun mk_name sel =
- Binding.name ("update_" ^ Long_Name.base_name (fst (dest_Const sel)))
+ Binding.name ("update_" ^ Long_Name.base_name (dest_Const_name sel))
val thms_binding = (Binding.name "record_simps", @{attributes [simp]})
@@ -193,7 +193,7 @@
val thms = flat (map (prove lthy'' update_defs update_ts) (0 upto len-1))
fun insert sel =
- Symtab.insert op = (fst (dest_Const sel), Local_Theory.full_name lthy' (mk_name sel))
+ Symtab.insert op = (dest_Const_name sel, Local_Theory.full_name lthy' (mk_name sel))
in
lthy''
|> Local_Theory.map_background_naming (Name_Space.mandatory_path short_name)
@@ -250,7 +250,7 @@
val {ctrs, selss, ...} = the (Ctr_Sugar.ctr_sugar_of ctxt typ_name)
val ctr = case ctrs of [ctr] => ctr | _ => error "BNF_Record.record_fields_tr: expected only single constructor"
val sels = case selss of [sels] => sels | _ => error "BNF_Record.record_fields_tr: expected selectors"
- val ctr_dummy = Const (fst (dest_Const ctr), dummyT)
+ val ctr_dummy = Const (dest_Const_name ctr, dummyT)
fun mk_arg name =
case AList.lookup op = assns' name of
@@ -258,7 +258,7 @@
| SOME t => t
in
if length assns = length sels then
- list_comb (ctr_dummy, map (mk_arg o fst o dest_Const) sels)
+ list_comb (ctr_dummy, map (mk_arg o dest_Const_name) sels)
else
error ("BNF_Record.record_fields_tr: expected " ^ Value.print_int (length sels) ^ " field(s)")
end
--- a/src/HOL/Library/old_recdef.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Library/old_recdef.ML Sun Aug 04 17:39:47 2024 +0200
@@ -1557,7 +1557,7 @@
* term "f v1..vn" which is a pattern that any full application
* of "f" will match.
*-------------------------------------------------------------*)
- val func_name = #1(dest_Const func)
+ val func_name = dest_Const_name func
fun is_func (Const (name,_)) = (name = func_name)
| is_func _ = false
val rcontext = rev cntxt
@@ -1730,7 +1730,7 @@
fold_rev (fn (row as (p::rst, rhs)) =>
fn (in_group,not_in_group) =>
let val (pc,args) = USyntax.strip_comb p
- in if (#1(dest_Const pc) = c)
+ in if (dest_Const_name pc = c)
then ((args@rst, rhs)::in_group, not_in_group)
else (in_group, row::not_in_group)
end) rows ([],[])
@@ -1768,7 +1768,7 @@
* Produce an instance of a constructor, plus genvars for its arguments.
*---------------------------------------------------------------------------*)
fun fresh_constr ty_match colty gv c =
- let val (_,Ty) = dest_Const c
+ let val Ty = dest_Const_type c
val L = binder_types Ty
and ty = body_type Ty
val ty_theta = ty_match ty colty
@@ -1786,7 +1786,7 @@
fold_rev (fn (row as ((prfx, p::rst), rhs)) =>
fn (in_group,not_in_group) =>
let val (pc,args) = USyntax.strip_comb p
- in if ((#1 (Term.dest_Const pc) = name) handle TERM _ => false)
+ in if ((dest_Const_name pc = name) handle TERM _ => false)
then (((prfx,args@rst), rhs)::in_group, not_in_group)
else (in_group, row::not_in_group) end)
rows ([],[]);
@@ -1801,7 +1801,7 @@
fun part {constrs = [], rows, A} = rev A
| part {constrs = c::crst, rows, A} =
let val (c',gvars) = fresh c
- val (in_group, not_in_group) = mk_group (#1 (dest_Const c')) rows
+ val (in_group, not_in_group) = mk_group (dest_Const_name c') rows
val in_group' =
if (null in_group) (* Constructor not given *)
then [((prfx, #2(fresh c)), (USyntax.ARB res_ty, (~1,false)))]
@@ -1884,7 +1884,7 @@
of NONE => mk_case_fail("Not a known datatype: "^ty_name)
| SOME{case_const,constructors} =>
let
- val case_const_name = #1(dest_Const case_const)
+ val case_const_name = dest_Const_name case_const
val nrows = maps (expand constructors pty) rows
val subproblems = divide(constructors, pty, range_ty, nrows)
val groups = map #group subproblems
@@ -2701,7 +2701,7 @@
local
val cong_head =
- fst o Term.dest_Const o Term.head_of o fst o Logic.dest_equals o Thm.concl_of;
+ dest_Const_name o Term.head_of o fst o Logic.dest_equals o Thm.concl_of;
fun prep_cong raw_thm =
let val thm = safe_mk_meta_eq raw_thm in (cong_head thm, thm) end;
--- a/src/HOL/List.thy Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/List.thy Sun Aug 04 17:39:47 2024 +0200
@@ -639,7 +639,7 @@
(case possible_index_of_singleton_case (fst (split_last args)) of
SOME i =>
let
- val constr_names = map (fst o dest_Const) ctrs
+ val constr_names = map dest_Const_name ctrs
val (Ts, _) = strip_type T
val T' = List.last Ts
in SOME (List.last args, T', i, nth args i, nth constr_names i) end
--- a/src/HOL/Nominal/nominal_inductive.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Sun Aug 04 17:39:47 2024 +0200
@@ -46,7 +46,7 @@
proc = fn _ => fn _ => fn ct =>
(case Thm.term_of ct of
Const (\<^const_name>\<open>Nominal.perm\<close>, _) $ _ $ t =>
- if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t))
+ if member (op =) names (the_default "" (try (dest_Const_name o head_of) t))
then SOME perm_bool else NONE
| _ => NONE),
identifier = []};
--- a/src/HOL/Nominal/nominal_inductive2.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML Sun Aug 04 17:39:47 2024 +0200
@@ -50,7 +50,7 @@
proc = fn _ => fn _ => fn ct =>
(case Thm.term_of ct of
Const (\<^const_name>\<open>Nominal.perm\<close>, _) $ _ $ t =>
- if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t))
+ if member (op =) names (the_default "" (try (dest_Const_name o head_of) t))
then SOME perm_bool else NONE
| _ => NONE),
identifier = []};
--- a/src/HOL/Real_Asymp/real_asymp.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Real_Asymp/real_asymp.ML Sun Aug 04 17:39:47 2024 +0200
@@ -53,7 +53,7 @@
fun prove_landau ectxt l f g =
let
val ctxt = get_ctxt ectxt
- val l' = l |> dest_Const |> fst
+ val l' = dest_Const_name l
val basis = Asymptotic_Basis.default_basis
val ([thm1, thm2], basis) = Exp.expand_terms ectxt [f, g] basis
val prover =
--- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML Sun Aug 04 17:39:47 2024 +0200
@@ -313,7 +313,7 @@
then should still be able to handle formulas like
(! X, X. F).*)
if x = bound_var andalso
- fst (dest_Const t1) = \<^const_name>\<open>All\<close> then
+ dest_Const_name t1 = \<^const_name>\<open>All\<close> then
(*Body might contain free variables, so bind them using "var_ctxt".
this involves replacing instances of Free with instances of Bound
at the right index.*)
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Sun Aug 04 17:39:47 2024 +0200
@@ -555,13 +555,12 @@
val (h, args) =
strip_comb t'
|> apfst (strip_abs #> snd #> strip_comb #> fst)
- val get_const_name = dest_Const #> fst
val h_property =
is_Free h orelse
is_Var h orelse
(is_Const h
- andalso (get_const_name h <> get_const_name \<^term>\<open>HOL.Ex\<close>)
- andalso (get_const_name h <> get_const_name \<^term>\<open>HOL.All\<close>)
+ andalso (dest_Const_name h <> dest_Const_name \<^term>\<open>HOL.Ex\<close>)
+ andalso (dest_Const_name h <> dest_Const_name \<^term>\<open>HOL.All\<close>)
andalso (h <> \<^term>\<open>Hilbert_Choice.Eps\<close>)
andalso (h <> \<^term>\<open>HOL.conj\<close>)
andalso (h <> \<^term>\<open>HOL.disj\<close>)
@@ -588,11 +587,10 @@
Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t' $ (Const (\<^const_name>\<open>Hilbert_Choice.Eps\<close>, _) $ _) =>
let
val (h, args) = strip_comb t'
- val get_const_name = dest_Const #> fst
val const_h_test =
if is_Const h then
- (get_const_name h = get_const_name \<^term>\<open>HOL.Ex\<close>)
- orelse (get_const_name h = get_const_name \<^term>\<open>HOL.All\<close>)
+ (dest_Const_name h = dest_Const_name \<^term>\<open>HOL.Ex\<close>)
+ orelse (dest_Const_name h = dest_Const_name \<^term>\<open>HOL.All\<close>)
orelse (h = \<^term>\<open>Hilbert_Choice.Eps\<close>)
orelse (h = \<^term>\<open>HOL.conj\<close>)
orelse (h = \<^term>\<open>HOL.disj\<close>)
@@ -898,9 +896,7 @@
*)
val filtered_candidates =
- map (dest_Const
- #> snd
- #> use_candidate skolem_const_ty params' [])
+ map (dest_Const_type #> use_candidate skolem_const_ty params' [])
consts_candidates (* prefiltered_candidates *)
|> pair consts_candidates (* prefiltered_candidates *)
|> ListPair.zip
@@ -1076,8 +1072,7 @@
#> HOLogic.dest_eq (*the unification constraint's "="*)
#> fst
#> head_of
- #> dest_Const
- #> snd
+ #> dest_Const_type
fun arity_of ty =
let
--- a/src/HOL/Tools/ATP/atp_util.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML Sun Aug 04 17:39:47 2024 +0200
@@ -181,7 +181,7 @@
fun varify_type ctxt T =
Variable.polymorphic_types ctxt [Const (\<^const_name>\<open>undefined\<close>, T)]
- |> snd |> the_single |> dest_Const |> snd
+ |> snd |> the_single |> dest_Const_type
(* TODO: use "Term_Subst.instantiateT" instead? *)
fun instantiate_type thy T1 T1' T2 =
--- a/src/HOL/Tools/BNF/bnf_def.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML Sun Aug 04 17:39:47 2024 +0200
@@ -1001,7 +1001,7 @@
fun note_bnf_defs bnf lthy =
let
fun mk_def_binding cst_of =
- Thm.def_binding (Binding.qualified_name (dest_Const (cst_of bnf) |> fst));
+ Thm.def_binding (Binding.qualified_name (dest_Const_name (cst_of bnf)));
val notes =
[(mk_def_binding map_of_bnf, map_def_of_bnf bnf),
(mk_def_binding rel_of_bnf, rel_def_of_bnf bnf),
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Sun Aug 04 17:39:47 2024 +0200
@@ -408,7 +408,7 @@
val xtor_un_fold_defs = map (Drule.abs_def o Morphism.thm phi) un_fold_defs;
val xtor_cache_defs = map (Drule.abs_def o Morphism.thm phi) cache_defs;
val xtor_un_folds' = map2 (fn raw => fn t =>
- Const (fst (dest_Const t), fold_strTs ---> fastype_of raw))
+ Const (dest_Const_name t, fold_strTs ---> fastype_of raw))
un_folds xtor_un_folds;
val fp_un_fold_o_maps = of_fp_res #xtor_un_fold_o_maps
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Sun Aug 04 17:39:47 2024 +0200
@@ -785,7 +785,7 @@
||> `Local_Theory.end_nested;
val phi = Proof_Context.export_morphism lthy_old lthy;
- val co_rec_names = map (fst o dest_Const o Morphism.term phi) co_rec_frees;
+ val co_rec_names = map (dest_Const_name o Morphism.term phi) co_rec_frees;
val co_recs = @{map 2} (fn name => fn resT =>
Const (name, co_rec_argTs ---> resT)) co_rec_names co_rec_resTs;
val co_rec_defs = map (fn def =>
--- a/src/HOL/Tools/BNF/bnf_gfp.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Sun Aug 04 17:39:47 2024 +0200
@@ -283,7 +283,7 @@
||> `Local_Theory.end_nested;
val phi = Proof_Context.export_morphism lthy_old lthy;
- val coalg = fst (Term.dest_Const (Morphism.term phi coalg_free));
+ val coalg = dest_Const_name (Morphism.term phi coalg_free);
val coalg_def = mk_unabs_def (2 * n) (HOLogic.mk_obj_eq (Morphism.thm phi coalg_def_free));
fun mk_coalg Bs ss =
@@ -372,7 +372,7 @@
||> `Local_Theory.end_nested;
val phi = Proof_Context.export_morphism lthy_old lthy;
- val mor = fst (Term.dest_Const (Morphism.term phi mor_free));
+ val mor = dest_Const_name (Morphism.term phi mor_free);
val mor_def = mk_unabs_def (5 * n) (HOLogic.mk_obj_eq (Morphism.thm phi mor_def_free));
fun mk_mor Bs1 ss1 Bs2 ss2 fs =
@@ -527,7 +527,7 @@
||> `Local_Theory.end_nested;
val phi = Proof_Context.export_morphism lthy_old lthy;
- val bis = fst (Term.dest_Const (Morphism.term phi bis_free));
+ val bis = dest_Const_name (Morphism.term phi bis_free);
val bis_def = mk_unabs_def (5 * n) (HOLogic.mk_obj_eq (Morphism.thm phi bis_def_free));
fun mk_bis Bs1 ss1 Bs2 ss2 Rs =
@@ -678,7 +678,7 @@
val lsbis_defs = map (fn def =>
mk_unabs_def (2 * n) (HOLogic.mk_obj_eq (Morphism.thm phi def))) lsbis_def_frees;
- val lsbiss = map (fst o Term.dest_Const o Morphism.term phi) lsbis_frees;
+ val lsbiss = map (dest_Const_name o Morphism.term phi) lsbis_frees;
fun mk_lsbis Bs ss i =
let
@@ -776,7 +776,7 @@
val phi = Proof_Context.export_morphism lthy_old lthy;
val sbd_def = HOLogic.mk_obj_eq (Morphism.thm phi sbd_def_free);
- val sbd = Const (fst (Term.dest_Const (Morphism.term phi sbd_free)), mk_relT (`I sbdT));
+ val sbd = Const (dest_Const_name (Morphism.term phi sbd_free), mk_relT (`I sbdT));
val Abs_sbdT_inj = mk_Abs_inj_thm (#Abs_inject sbdT_loc_info);
val Abs_sbdT_bij = mk_Abs_bij_thm lthy Abs_sbdT_inj (#Abs_cases sbdT_loc_info);
@@ -895,7 +895,7 @@
val isNode_defs = map (fn def =>
mk_unabs_def 3 (HOLogic.mk_obj_eq (Morphism.thm phi def))) isNode_def_frees;
- val isNodes = map (fst o Term.dest_Const o Morphism.term phi) isNode_frees;
+ val isNodes = map (dest_Const_name o Morphism.term phi) isNode_frees;
fun mk_isNode kl i =
Term.list_comb (Const (nth isNodes (i - 1), isNodeT), [Kl, lab, kl]);
@@ -933,7 +933,7 @@
val phi = Proof_Context.export_morphism lthy_old lthy;
val carT_defs = map (fn def => HOLogic.mk_obj_eq (Morphism.thm phi def)) carT_def_frees;
- val carTs = map (fst o Term.dest_Const o Morphism.term phi) carT_frees;
+ val carTs = map (dest_Const_name o Morphism.term phi) carT_frees;
fun mk_carT i = Const (nth carTs (i - 1), HOLogic.mk_setT treeT);
@@ -969,7 +969,7 @@
val strT_defs = map (fn def =>
trans OF [HOLogic.mk_obj_eq (Morphism.thm phi def) RS fun_cong, @{thm prod.case}])
strT_def_frees;
- val strTs = map (fst o Term.dest_Const o Morphism.term phi) strT_frees;
+ val strTs = map (dest_Const_name o Morphism.term phi) strT_frees;
fun mk_strT FT i = Const (nth strTs (i - 1), treeT --> FT);
@@ -1034,7 +1034,7 @@
val phi = Proof_Context.export_morphism lthy_old lthy;
val Lev_def = mk_unabs_def n (HOLogic.mk_obj_eq (Morphism.thm phi Lev_def_free));
- val Lev = fst (Term.dest_Const (Morphism.term phi Lev_free));
+ val Lev = dest_Const_name (Morphism.term phi Lev_free);
fun mk_Lev ss nat i =
let
@@ -1078,7 +1078,7 @@
val phi = Proof_Context.export_morphism lthy_old lthy;
val rv_def = mk_unabs_def n (HOLogic.mk_obj_eq (Morphism.thm phi rv_def_free));
- val rv = fst (Term.dest_Const (Morphism.term phi rv_free));
+ val rv = dest_Const_name (Morphism.term phi rv_free);
fun mk_rv ss kl i =
let
@@ -1124,7 +1124,7 @@
val beh_defs = map (fn def =>
mk_unabs_def (n + 1) (HOLogic.mk_obj_eq (Morphism.thm phi def))) beh_def_frees;
- val behs = map (fst o Term.dest_Const o Morphism.term phi) beh_frees;
+ val behs = map (dest_Const_name o Morphism.term phi) beh_frees;
fun mk_beh ss i =
let
@@ -1447,7 +1447,7 @@
val phi = Proof_Context.export_morphism lthy_old lthy;
val unfolds = map (Morphism.term phi) unfold_frees;
- val unfold_names = map (fst o dest_Const) unfolds;
+ val unfold_names = map dest_Const_name unfolds;
fun mk_unfolds passives actives =
@{map 3} (fn name => fn T => fn active =>
Const (name, Library.foldr (op -->)
@@ -1753,7 +1753,7 @@
val phi = Proof_Context.export_morphism lthy_old lthy;
val col_defs = map (fn def => HOLogic.mk_obj_eq (Morphism.thm phi def)) col_def_frees;
- val cols = map (fst o Term.dest_Const o Morphism.term phi) col_frees;
+ val cols = map (dest_Const_name o Morphism.term phi) col_frees;
fun mk_col Ts nat i j T =
let
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Sun Aug 04 17:39:47 2024 +0200
@@ -176,7 +176,7 @@
fun coinduct_extras_of_generic context =
corec_infos_of_generic context
- #> map (#corecUU #> dest_Const #> fst #> Symtab.lookup (#2 (Data.get context)) #> the
+ #> map (#corecUU #> dest_Const_name #> Symtab.lookup (#2 (Data.get context)) #> the
#> transfer_coinduct_extra (Context.theory_of context));
fun get_coinduct_uptos fpT_name context =
@@ -628,7 +628,7 @@
val fpT as Type (_, fp_argTs) = range_type (fastype_of algrho);
fun has_algrho (\<^Const_>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ rhs)) =
- fst (dest_Const (head_of (strip_abs_body rhs))) = algrho_name;
+ dest_Const_name (head_of (strip_abs_body rhs)) = algrho_name;
val eq_algrho :: _ =
maps (filter (has_algrho o Thm.prop_of) o #eq_algrhos o snd) (all_friend_extras_of ctxt);
@@ -955,7 +955,7 @@
| find_all_associated_types ((T1, T2) :: TTs) T =
find_all_associated_types TTs T |> T1 = T ? cons T2;
-fun as_member_of tab = try dest_Const #> Option.mapPartial (fst #> Symtab.lookup tab);
+fun as_member_of tab = try dest_Const_name #> Option.mapPartial (Symtab.lookup tab);
fun extract_rho_from_equation
({ctr_guards, inner_buffer = {Oper, VLeaf, CLeaf, ctr_wrapper, friends}, ...},
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML Sun Aug 04 17:39:47 2024 +0200
@@ -394,7 +394,7 @@
|> perhaps (try HOLogic.dest_Trueprop)
|> HOLogic.dest_eq
|>> fst o strip_comb
- |>> fst o dest_Const
+ |>> dest_Const_name
||> fst o dest_comb
||> snd o strip_comb
||> map (map_types (XifyT o substAT));
@@ -429,9 +429,9 @@
if forall is_some sels then SOME (disc, map the sels) else NONE;
val pattern_ctrs = (ctrs0, selss0)
- ||> map (map (try dest_Const #> Option.mapPartial (fst #> Symtab.lookup sels)))
+ ||> map (map (try dest_Const_name #> Option.mapPartial (Symtab.lookup sels)))
||> @{map 2} mk_disc_sels_pair all_discs
- |>> map (dest_Const #> fst)
+ |>> map dest_Const_name
|> op ~~
|> map_filter (fn (s, opt) => if is_some opt then SOME (s, the opt) else NONE)
|> Symtab.make;
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Sun Aug 04 17:39:47 2024 +0200
@@ -921,7 +921,7 @@
let val (u, vs) = strip_comb t in
if is_Free u andalso has_call u then
Inr_const T U2 $ mk_tuple1_balanced bound_Ts vs
- else if try (fst o dest_Const) u = SOME \<^const_name>\<open>case_prod\<close> then
+ else if try dest_Const_name u = SOME \<^const_name>\<open>case_prod\<close> then
map (rewrite bound_Ts) vs |> chop 1
|>> HOLogic.mk_case_prod o the_single
|> Term.list_comb
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Sun Aug 04 17:39:47 2024 +0200
@@ -243,7 +243,7 @@
||> `Local_Theory.end_nested;
val phi = Proof_Context.export_morphism lthy_old lthy;
- val alg = fst (Term.dest_Const (Morphism.term phi alg_free));
+ val alg = dest_Const_name (Morphism.term phi alg_free);
val alg_def = mk_unabs_def (2 * n) (HOLogic.mk_obj_eq (Morphism.thm phi alg_def_free));
fun mk_alg Bs ss =
@@ -335,7 +335,7 @@
||> `Local_Theory.end_nested;
val phi = Proof_Context.export_morphism lthy_old lthy;
- val mor = fst (Term.dest_Const (Morphism.term phi mor_free));
+ val mor = dest_Const_name (Morphism.term phi mor_free);
val mor_def = mk_unabs_def (5 * n) (HOLogic.mk_obj_eq (Morphism.thm phi mor_def_free));
fun mk_mor Bs1 ss1 Bs2 ss2 fs =
@@ -480,7 +480,7 @@
val phi = Proof_Context.export_morphism lthy_old lthy;
val sbd_def = HOLogic.mk_obj_eq (Morphism.thm phi sbd_def_free);
- val sbd = Const (fst (Term.dest_Const (Morphism.term phi sbd_free)), mk_relT (`I sbdT));
+ val sbd = Const (dest_Const_name (Morphism.term phi sbd_free), mk_relT (`I sbdT));
val Abs_sbdT_inj = mk_Abs_inj_thm (#Abs_inject sbdT_loc_info);
@@ -670,7 +670,7 @@
||> `Local_Theory.end_nested;
val phi = Proof_Context.export_morphism lthy_old lthy;
- val min_algs = map (fst o Term.dest_Const o Morphism.term phi) min_alg_frees;
+ val min_algs = map (dest_Const_name o Morphism.term phi) min_alg_frees;
val min_alg_defs = map (fn def =>
mk_unabs_def n (HOLogic.mk_obj_eq (Morphism.thm phi def))) min_alg_def_frees;
@@ -1016,7 +1016,7 @@
val phi = Proof_Context.export_morphism lthy_old lthy;
val folds = map (Morphism.term phi) fold_frees;
- val fold_names = map (fst o dest_Const) folds;
+ val fold_names = map dest_Const_name folds;
fun mk_folds passives actives =
@{map 3} (fn name => fn T => fn active =>
Const (name, Library.foldr (op -->)
@@ -1408,8 +1408,7 @@
val phi = Proof_Context.export_morphism lthy_old lthy;
val sbd0_def = HOLogic.mk_obj_eq (Morphism.thm phi sbd0_def_free);
- val sbd0 = Const (fst (Term.dest_Const (Morphism.term phi sbd0_free)),
- mk_relT (`I sbd0T));
+ val sbd0 = Const (dest_Const_name (Morphism.term phi sbd0_free), mk_relT (`I sbd0T));
val Abs_sbd0T_inj = mk_Abs_inj_thm (#Abs_inject sbd0T_loc_info);
val Abs_sbd0T_bij = mk_Abs_bij_thm lthy Abs_sbd0T_inj (#Abs_cases sbd0T_loc_info);
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Sun Aug 04 17:39:47 2024 +0200
@@ -321,7 +321,7 @@
else
not_datatype_name fpT_name1;
- val rec'_names = map (fst o dest_Const) recs';
+ val rec'_names = map dest_Const_name recs';
val rec'_thms = flat rec'_thmss;
fun mk_info (kk, {T = Type (T_name0, _), fp_ctr_sugar = {ctr_sugar = {casex, exhaust, nchotomy,
@@ -330,7 +330,7 @@
(T_name0,
{index = kk, descr = descr, inject = injects, distinct = distincts, induct = induct',
inducts = inducts', exhaust = exhaust, nchotomy = nchotomy, rec_names = rec'_names,
- rec_rewrites = rec'_thms, case_name = fst (dest_Const casex), case_rewrites = case_thms,
+ rec_rewrites = rec'_thms, case_name = dest_Const_name casex, case_rewrites = case_thms,
case_cong = case_cong, case_cong_weak = case_cong_weak, split = split,
split_asm = split_asm});
--- a/src/HOL/Tools/BNF/bnf_lift.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Tools/BNF/bnf_lift.ML Sun Aug 04 17:39:47 2024 +0200
@@ -921,7 +921,7 @@
|> fst;
(* create local definitions `b = tm` with n arguments *)
- fun suffix tm s = (dest_Const tm |> fst |> Long_Name.base_name) ^ s;
+ fun suffix tm s = Long_Name.base_name (dest_Const_name tm) ^ s;
fun define lthy b n tm =
let
val b = Binding.qualify true absT_name (Binding.qualified_name b);
--- a/src/HOL/Tools/Ctr_Sugar/case_translation.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/case_translation.ML Sun Aug 04 17:39:47 2024 +0200
@@ -122,7 +122,7 @@
fun case_error s = error ("Error in case expression:\n" ^ s);
-val name_of = try (dest_Const #> fst);
+val name_of = try dest_Const_name;
(* parse translation *)
@@ -217,8 +217,8 @@
val ctxt = Context.proof_of context;
val case_comb = singleton (Variable.polymorphic ctxt) raw_case_comb;
val constrs = Variable.polymorphic ctxt raw_constrs;
- val case_key = case_comb |> dest_Const |> fst;
- val constr_keys = map (fst o dest_Const) constrs;
+ val case_key = dest_Const_name case_comb;
+ val constr_keys = map dest_Const_name constrs;
val data = (case_comb, constrs);
val Tname = Tname_of_data data;
val update_constrs = fold (fn key => Symtab.cons_list (key, (Tname, data))) constr_keys;
@@ -258,7 +258,7 @@
(*Produce an instance of a constructor, plus fresh variables for its arguments.*)
fun fresh_constr colty used c =
let
- val (_, T) = dest_Const c;
+ val T = dest_Const_type c;
val Ts = binder_types T;
val (names, _) = fold_map Name.variant (make_tnames Ts) used;
val ty = body_type T;
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Sun Aug 04 17:39:47 2024 +0200
@@ -362,7 +362,7 @@
|> HOLogic.dest_eq
|>> (Term.dest_comb
#>> const_or_free_name
- ##> (Term.strip_comb #>> (Term.dest_Const #> fst)))
+ ##> (Term.strip_comb #>> dest_Const_name))
handle TERM _ => malformed ();
in
if forall (is_Free orf is_Var) vars andalso not (has_duplicates (op aconv) vars) then
--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Sun Aug 04 17:39:47 2024 +0200
@@ -276,7 +276,7 @@
val qty_code_dt_bundle_name = bundle_name_of_rep_isom_data rep_isom_data
val rep_isom = mk_rep_isom_of_code_dt qty_ret code_dt |> the
val lthy3 = if quot_active then lthy2 else Bundle.includes [qty_code_dt_bundle_name] lthy2
- fun qty_isom_of_rep_isom rep = rep |> dest_Const |> snd |> domain_type
+ fun qty_isom_of_rep_isom rep = domain_type (dest_Const_type rep)
val qty_isom = qty_isom_of_rep_isom rep_isom
val f'_var = (Binding.suffix_name "_aux" (fst var), NoSyn);
val f'_qty = strip_type qty |> fst |> rpair qty_isom |> op --->
@@ -360,8 +360,8 @@
val ctr_sugar = fp |> #fp_ctr_sugar |> #ctr_sugar
val ctrs = map (Ctr_Sugar.mk_ctr typs) (#ctrs ctr_sugar);
val qty_ctrs = map (Ctr_Sugar.mk_ctr qty_typs) (#ctrs ctr_sugar);
- val ctr_Tss = map (dest_Const #> snd #> binder_types) ctrs;
- val qty_ctr_Tss = map (dest_Const #> snd #> binder_types) qty_ctrs;
+ val ctr_Tss = map (binder_types o dest_Const_type) ctrs;
+ val qty_ctr_Tss = map (binder_types o dest_Const_type) qty_ctrs;
val n = length ctrs;
val ks = 1 upto n;
@@ -478,14 +478,14 @@
fun mk_ctr ctr ctr_Ts sels =
let
- val sel_ret_Ts = map (dest_Const #> snd #> body_type) sels;
+ val sel_ret_Ts = map (body_type o dest_Const_type) sels;
fun rep_isom lthy t (rty, qty) =
let
val rep = quot_isom_rep lthy (rty, qty)
in
- if is_Const rep andalso (rep |> dest_Const |> fst) = \<^const_name>\<open>id\<close> then
- t else rep $ t
+ if is_Const rep andalso dest_Const_name rep = \<^const_name>\<open>id\<close>
+ then t else rep $ t
end;
in
@{fold 3} (fn sel => fn ctr_T => fn sel_ret_T => fn ctr =>
--- a/src/HOL/Tools/Lifting/lifting_info.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Tools/Lifting/lifting_info.ML Sun Aug 04 17:39:47 2024 +0200
@@ -392,7 +392,7 @@
val pol_mono_rule = introduce_polarities mono_rule
val mono_ruleT_name =
dest_Type_name (fst (relation_types (fst (relation_types
- (snd (dest_Const (head_of (HOLogic.dest_Trueprop (Thm.concl_of pol_mono_rule)))))))))
+ (dest_Const_type (head_of (HOLogic.dest_Trueprop (Thm.concl_of pol_mono_rule))))))))
in
if Symtab.defined (get_relator_distr_data' context) mono_ruleT_name
then
@@ -419,7 +419,7 @@
let
val distr_ruleT_name =
dest_Type_name (fst (relation_types (fst (relation_types
- (snd (dest_Const (head_of (HOLogic.dest_Trueprop (Thm.concl_of distr_rule)))))))))
+ (dest_Const_type (head_of (HOLogic.dest_Trueprop (Thm.concl_of distr_rule))))))))
in
if Symtab.defined (get_relator_distr_data' context) distr_ruleT_name then
(Data.map o map_relator_distr_data)
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Sun Aug 04 17:39:47 2024 +0200
@@ -338,9 +338,8 @@
fun make_goal pcr_def constr =
let
- val pred_name =
- (fst o dest_Const o strip_args 1 o HOLogic.dest_Trueprop o Thm.prop_of) constr
- val arg = (fst o Logic.dest_equals o Thm.prop_of) pcr_def
+ val pred_name = dest_Const_name (strip_args 1 (HOLogic.dest_Trueprop (Thm.prop_of constr)))
+ val arg = fst (Logic.dest_equals (Thm.prop_of pcr_def))
in
HOLogic.mk_Trueprop ((Const (pred_name, (fastype_of arg) --> HOLogic.boolT)) $ arg)
end
@@ -360,7 +359,8 @@
let
val prems = map HOLogic.dest_Trueprop (Thm.prems_of thm)
val thm_name =
- (Long_Name.base_name o fst o dest_Const o strip_args 1 o HOLogic.dest_Trueprop o Thm.concl_of) thm
+ Long_Name.base_name
+ (dest_Const_name (strip_args 1 (HOLogic.dest_Trueprop (Thm.concl_of thm))))
val non_trivial_assms = filter_out is_trivial_assm prems
in
if null non_trivial_assms then ()
@@ -941,7 +941,7 @@
fun filter_transfer_rules_by_rel transfer_rel transfer_rules =
let
- val transfer_rel_name = transfer_rel |> dest_Const |> fst;
+ val transfer_rel_name = dest_Const_name transfer_rel;
fun has_transfer_rel thm =
let
val concl = thm |> Thm.concl_of |> HOLogic.dest_Trueprop
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Sun Aug 04 17:39:47 2024 +0200
@@ -601,7 +601,7 @@
\<^type_name>\<open>integer\<close>]
fun repair_constr_type (Type (_, Ts)) T =
- snd (dest_Const (Ctr_Sugar.mk_ctr Ts (Const (Name.uu, T))))
+ dest_Const_type (Ctr_Sugar.mk_ctr Ts (Const (Name.uu, T)))
fun register_frac_type_generic frac_s ersaetze generic =
let
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Sun Aug 04 17:39:47 2024 +0200
@@ -90,28 +90,27 @@
fun add_wacky_syntax ctxt =
let
- val name_of = fst o dest_Const
val thy = Proof_Context.theory_of ctxt
val (unrep_s, thy) = thy
|> Sign.declare_const_global ((\<^binding>\<open>nitpick_unrep\<close>, \<^typ>\<open>'a\<close>),
mixfix (unrep_mixfix (), [], 1000))
- |>> name_of
+ |>> dest_Const_name
val (maybe_s, thy) = thy
|> Sign.declare_const_global ((\<^binding>\<open>nitpick_maybe\<close>, \<^typ>\<open>'a => 'a\<close>),
mixfix (maybe_mixfix (), [1000], 1000))
- |>> name_of
+ |>> dest_Const_name
val (abs_s, thy) = thy
|> Sign.declare_const_global ((\<^binding>\<open>nitpick_abs\<close>, \<^typ>\<open>'a => 'b\<close>),
mixfix (abs_mixfix (), [40], 40))
- |>> name_of
+ |>> dest_Const_name
val (base_s, thy) = thy
|> Sign.declare_const_global ((\<^binding>\<open>nitpick_base\<close>, \<^typ>\<open>'a => 'a\<close>),
mixfix (base_mixfix (), [1000], 1000))
- |>> name_of
+ |>> dest_Const_name
val (step_s, thy) = thy
|> Sign.declare_const_global ((\<^binding>\<open>nitpick_step\<close>, \<^typ>\<open>'a => 'a\<close>),
mixfix (step_mixfix (), [1000], 1000))
- |>> name_of
+ |>> dest_Const_name
in
(((unrep_s, maybe_s, abs_s), (base_s, step_s)),
Proof_Context.transfer thy ctxt)
--- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Sun Aug 04 17:39:47 2024 +0200
@@ -359,7 +359,7 @@
map2 prove_cases newTs (Old_Datatype_Prop.make_cases case_names0 descr thy2);
fun case_name_of (th :: _) =
- fst (dest_Const (head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of th))))));
+ dest_Const_name (head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of th)))));
val case_names = map case_name_of case_thms;
in
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Sun Aug 04 17:39:47 2024 +0200
@@ -446,7 +446,7 @@
let
val (p, args) = strip_comb t
val mode = Predicate_Compile_Core.head_mode_of derivation
- val name = fst (dest_Const p)
+ val name = dest_Const_name p
val p' = the (AList.lookup (op =) moded_pred_table' (name, (pol, mode)))
val args' = map (translate_term ctxt constant_table') args
--- a/src/HOL/Tools/Predicate_Compile/core_data.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Tools/Predicate_Compile/core_data.ML Sun Aug 04 17:39:47 2024 +0200
@@ -274,7 +274,7 @@
fun is_intro_of intro =
let
val (const, _) = strip_comb (HOLogic.dest_Trueprop (Thm.concl_of intro))
- in (fst (dest_Const const) = name) end;
+ in dest_Const_name const = name end;
val intros = map (preprocess_intro thy) (filter is_intro_of (#intrs result))
val index = find_index (fn s => s = name) (#names (fst info))
val pre_elim = nth (#elims result) index
@@ -310,7 +310,7 @@
fun add_intro (opt_case_name, thm) thy =
let
- val (name, _) = dest_Const (fst (strip_intro_concl thm))
+ val name = dest_Const_name (fst (strip_intro_concl thm))
fun cons_intro gr =
(case try (Graph.get_node gr) name of
SOME _ =>
@@ -325,8 +325,7 @@
fun set_elim thm =
let
- val (name, _) =
- dest_Const (fst (strip_comb (HOLogic.dest_Trueprop (hd (Thm.prems_of thm)))))
+ val name = dest_Const_name (fst (strip_comb (HOLogic.dest_Trueprop (hd (Thm.prems_of thm)))))
in
PredData.map (Graph.map_node name (map_pred_data (apsnd (apfst (apfst (apsnd (K (SOME thm))))))))
end
@@ -346,7 +345,7 @@
fun register_intros (constname, pre_intros) thy =
let
val T = Sign.the_const_type thy constname
- fun constname_of_intro intr = fst (dest_Const (fst (strip_intro_concl intr)))
+ fun constname_of_intro intr = dest_Const_name (fst (strip_intro_concl intr))
val _ = if not (forall (fn intr => constname_of_intro intr = constname) pre_intros) then
error ("register_intros: Introduction rules of different constants are used\n" ^
"expected rules for " ^ constname ^ ", but received rules for " ^
--- a/src/HOL/Tools/Predicate_Compile/mode_inference.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Tools/Predicate_Compile/mode_inference.ML Sun Aug 04 17:39:47 2024 +0200
@@ -283,8 +283,8 @@
| rev_option_ord ord (SOME x, SOME y) = ord (x, y)
fun random_mode_in_deriv modes t deriv =
- case try dest_Const (fst (strip_comb t)) of
- SOME (s, _) =>
+ case try dest_Const_name (fst (strip_comb t)) of
+ SOME s =>
(case AList.lookup (op =) modes s of
SOME ms =>
(case AList.lookup (op =) (map (fn ((_, m), r) => (m, r)) ms) (head_mode_of deriv) of
@@ -316,7 +316,7 @@
fun fun_ord ((t1, deriv1, _), (t2, deriv2, _)) =
let
fun is_functional t mode =
- case try (fst o dest_Const o fst o strip_comb) t of
+ case try (dest_Const_name o fst o strip_comb) t of
NONE => false
| SOME c => is_some (Core_Data.alternative_compilation_of ctxt c mode)
in
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Sun Aug 04 17:39:47 2024 +0200
@@ -86,7 +86,7 @@
let
fun get_specs ts = map_filter (fn t =>
Term_Graph.get_node gr t |>
- (fn ths => if null ths then NONE else SOME (fst (dest_Const t), ths)))
+ (fn ths => if null ths then NONE else SOME (dest_Const_name t, ths)))
ts
val _ = print_step options ("Preprocessing scc of " ^
commas (map (Syntax.string_of_term_global thy) ts))
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Sun Aug 04 17:39:47 2024 +0200
@@ -951,7 +951,7 @@
fun case_betapply thy t =
let
- val case_name = fst (dest_Const (fst (strip_comb t)))
+ val case_name = dest_Const_name (fst (strip_comb t))
val Tcon = datatype_name_of_case_name thy case_name
val th = instantiated_case_rewrite thy Tcon
in
@@ -1068,7 +1068,7 @@
let
val subst = Sign.typ_match thy (fastype_of pred', fastype_of pred) Vartab.empty
handle Type.TYPE_MATCH =>
- error ("Type mismatch of predicate " ^ fst (dest_Const pred) ^
+ error ("Type mismatch of predicate " ^ dest_Const_name pred ^
" (trying to match " ^ Syntax.string_of_typ ctxt' (fastype_of pred') ^
" and " ^ Syntax.string_of_typ ctxt' (fastype_of pred) ^ ")" ^
" in " ^ Thm.string_of_thm ctxt' th)
@@ -1077,7 +1077,7 @@
let
val (pred', _) = strip_intro_concl th
val _ =
- if not (fst (dest_Const pred) = fst (dest_Const pred')) then
+ if not (dest_Const_name pred = dest_Const_name pred') then
raise Fail "Trying to instantiate another predicate"
else ()
val instT =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sun Aug 04 17:39:47 2024 +0200
@@ -1259,7 +1259,7 @@
| (intr :: _) =>
let
val (p, args) = strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl intr))
- val one_mode = hd (the (AList.lookup (op =) all_modes (fst (dest_Const p))))
+ val one_mode = hd (the (AList.lookup (op =) all_modes (dest_Const_name p)))
in
ho_args_of one_mode args
end)
@@ -1287,7 +1287,7 @@
let
val concl = Logic.strip_imp_concl (prop_of intro)
val (p, args) = strip_comb (HOLogic.dest_Trueprop concl)
- val params = fst (chop (nparams_of thy (fst (dest_Const p))) args)
+ val params = fst (chop (nparams_of thy (dest_Const_name p)) args)
fun check_arg arg = case HOLogic.strip_tupleT (fastype_of arg) of
(Ts as _ :: _ :: _) =>
if length (HOLogic.strip_tuple arg) = length Ts then
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Sun Aug 04 17:39:47 2024 +0200
@@ -198,10 +198,10 @@
val ctxt = Proof_Context.init_global thy
fun filtering th =
if is_equationlike th andalso
- defining_const_of_equation (normalize_equation thy th) = fst (dest_Const t) then
+ defining_const_of_equation (normalize_equation thy th) = dest_Const_name t then
SOME (normalize_equation thy th)
else
- if is_introlike th andalso defining_const_of_introrule th = fst (dest_Const t) then
+ if is_introlike th andalso defining_const_of_introrule th = dest_Const_name t then
SOME th
else
NONE
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Sun Aug 04 17:39:47 2024 +0200
@@ -39,7 +39,7 @@
fun pred_of_function thy name =
(case Item_Net.retrieve (Fun_Pred.get thy) (Const (name, dummyT)) of
[] => NONE
- | [(_, p)] => SOME (fst (dest_Const p))
+ | [(_, p)] => SOME (dest_Const_name p)
| _ => error ("Multiple matches possible for lookup of constant " ^ name))
fun defined_const thy name = is_some (pred_of_function thy name)
@@ -87,8 +87,8 @@
end;
fun keep_functions thy t =
- (case try dest_Const (fst (strip_comb t)) of
- SOME (c, _) => Predicate_Compile_Data.keep_function thy c
+ (case try dest_Const_name (fst (strip_comb t)) of
+ SOME c => Predicate_Compile_Data.keep_function thy c
| _ => false)
fun flatten thy lookup_pred t (names, prems) =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Sun Aug 04 17:39:47 2024 +0200
@@ -270,8 +270,8 @@
end
fun flat_intro intro (new_defs, thy) =
let
- val constname = fst (dest_Const (fst (strip_comb
- (HOLogic.dest_Trueprop (Logic.strip_imp_concl (Thm.prop_of intro))))))
+ val constname = dest_Const_name (fst (strip_comb
+ (HOLogic.dest_Trueprop (Logic.strip_imp_concl (Thm.prop_of intro)))))
val (intro_ts, (new_defs, thy)) =
fold_map_atoms (process constname) (Thm.prop_of intro) (new_defs, thy)
val th = Skip_Proof.make_thm thy intro_ts
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Sun Aug 04 17:39:47 2024 +0200
@@ -68,7 +68,7 @@
let
val name =
singleton (Name.variant_list names)
- ("specialised_" ^ Long_Name.base_name (fst (dest_Const pred)))
+ ("specialised_" ^ Long_Name.base_name (dest_Const_name pred))
val bname = Sign.full_bname thy name
in
if Sign.declared_const thy bname then
--- a/src/HOL/Tools/Quotient/quotient_term.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML Sun Aug 04 17:39:47 2024 +0200
@@ -67,8 +67,8 @@
fun get_mapfun_data ctxt s =
(case Symtab.lookup (Functor.entries ctxt) s of
- SOME [map_data] => (case try dest_Const (#mapper map_data) of
- SOME (c, _) => (Const (c, dummyT), #variances map_data)
+ SOME [map_data] => (case try dest_Const_name (#mapper map_data) of
+ SOME c => (Const (c, dummyT), #variances map_data)
| NONE => raise LIFT_MATCH ("map function for type " ^ quote s ^ " is not a constant."))
| SOME _ => raise LIFT_MATCH ("map function for type " ^ quote s ^ " is non-singleton entry.")
| NONE => raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found."))
--- a/src/HOL/Tools/SMT/smt_datatypes.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Tools/SMT/smt_datatypes.ML Sun Aug 04 17:39:47 2024 +0200
@@ -140,7 +140,7 @@
([], _) => (dss, ctxt1)
| (ds, ctxt2) =>
let
- val constrTs = maps (map (snd o Term.dest_Const o fst) o snd o snd) ds
+ val constrTs = maps (map (dest_Const_type o fst) o snd o snd) ds
val Us = fold (union (op =) o Term.binder_types) constrTs []
fun ins [] = [(Us, ds)]
--- a/src/HOL/Tools/Transfer/transfer.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Tools/Transfer/transfer.ML Sun Aug 04 17:39:47 2024 +0200
@@ -238,7 +238,7 @@
| is_eq _ = false
val add_eqs = Term.fold_aterms (fn t => if is_eq t then insert (op =) t else I)
val eq_consts = rev (add_eqs t [])
- val eqTs = map (snd o dest_Const) eq_consts
+ val eqTs = map dest_Const_type eq_consts
val used = Term.add_free_names prop []
val names = map (K "") eqTs |> Name.variant_list used
val frees = map Free (names ~~ eqTs)
@@ -322,7 +322,7 @@
val prop = Thm.prop_of thm
val (t, mk_prop') = dest prop
val Domainp_tms = rev (fold_Domainp (fn t => insert op= t) t [])
- val Domainp_Ts = map (snd o dest_funT o snd o dest_Const o fst o dest_comb) Domainp_tms
+ val Domainp_Ts = map (snd o dest_funT o dest_Const_type o fst o dest_comb) Domainp_tms
val used = Term.add_free_names t []
val rels = map (snd o dest_comb) Domainp_tms
val rel_names = map (fst o fst o dest_Var) rels
--- a/src/HOL/Tools/Transfer/transfer_bnf.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML Sun Aug 04 17:39:47 2024 +0200
@@ -70,7 +70,7 @@
let
val constr_name =
constraint_def |> Thm.prop_of |> HOLogic.dest_Trueprop |> fst o HOLogic.dest_eq
- |> head_of |> fst o dest_Const
+ |> head_of |> dest_Const_name
val live = live_of_bnf bnf
val (((As, Bs), Ds), ctxt') = ctxt
|> mk_TFrees live
--- a/src/HOL/Tools/choice_specification.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Tools/choice_specification.ML Sun Aug 04 17:39:47 2024 +0200
@@ -128,11 +128,11 @@
fun mk_exist c prop =
let
val T = type_of c
- val cname = Long_Name.base_name (fst (dest_Const c))
+ val cname = Long_Name.base_name (dest_Const_name c)
val vname = if Symbol_Pos.is_identifier cname then cname else "x"
in HOLogic.exists_const T $ Abs(vname,T,Term.abstract_over (c, prop)) end
val ex_prop = fold_rev mk_exist proc_consts prop
- val cnames = map (fst o dest_Const) proc_consts
+ val cnames = map dest_Const_name proc_consts
fun post_process (arg as (thy,thm)) =
let
fun inst_all thy v thm =
--- a/src/HOL/Tools/datatype_simprocs.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Tools/datatype_simprocs.ML Sun Aug 04 17:39:47 2024 +0200
@@ -37,7 +37,7 @@
fun mk_ctor T_names t =
let
- val name = t |> dest_Const |> fst
+ val name = dest_Const_name t
val (argTs, _) = strip_type (fastype_of t)
val active_poss = map (contains_datatypes T_names) argTs
in
--- a/src/HOL/Tools/inductive.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Tools/inductive.ML Sun Aug 04 17:39:47 2024 +0200
@@ -1237,7 +1237,7 @@
(* read off arities of inductive predicates from raw induction rule *)
fun arities_of induct =
map (fn (_ $ t $ u) =>
- (fst (dest_Const (head_of t)), length (snd (strip_comb u))))
+ (dest_Const_name (head_of t), length (snd (strip_comb u))))
(HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of induct)));
(* read off parameters of inductive predicate from raw induction rule *)
@@ -1251,7 +1251,7 @@
end;
val pname_of_intr =
- Thm.concl_of #> HOLogic.dest_Trueprop #> head_of #> dest_Const #> fst;
+ Thm.concl_of #> HOLogic.dest_Trueprop #> head_of #> dest_Const_name;
(* partition introduction rules according to predicate name *)
fun gen_partition_rules f induct intros =
--- a/src/HOL/Tools/inductive_realizer.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Sun Aug 04 17:39:47 2024 +0200
@@ -31,7 +31,7 @@
let val ys = subsets xs
in ys @ map (cons x) ys end;
-val pred_of = fst o dest_Const o head_of;
+val pred_of = dest_Const_name o head_of;
fun strip_all' used names (Const (\<^const_name>\<open>Pure.all\<close>, _) $ Abs (s, T, t)) =
let val (s', names') = (case names of
@@ -316,7 +316,7 @@
val rec_thms =
if null dt_names then []
else #rec_rewrites (BNF_LFP_Compat.the_info thy2 [] (hd dt_names));
- val rec_names = distinct (op =) (map (fst o dest_Const o head_of o fst o
+ val rec_names = distinct (op =) (map (dest_Const_name o head_of o fst o
HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) rec_thms);
val (constrss, _) = fold_map (fn (s, rs) => fn (recs, dummies) =>
if member (op =) rsets s then
@@ -422,7 +422,7 @@
(** realizer for elimination rules **)
- val case_names = map (fst o dest_Const o head_of o fst o HOLogic.dest_eq o
+ val case_names = map (dest_Const_name o head_of o fst o HOLogic.dest_eq o
HOLogic.dest_Trueprop o Thm.prop_of o hd) case_thms;
fun add_elim_realizer Ps
--- a/src/HOL/Tools/lin_arith.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Tools/lin_arith.ML Sun Aug 04 17:39:47 2024 +0200
@@ -177,7 +177,7 @@
(SOME s', SOME t') => SOME (mC $ s' $ t')
| (SOME s', NONE) => SOME s'
| (NONE, SOME t') =>
- SOME (mC $ Const (\<^const_name>\<open>Groups.one\<close>, domain_type (snd (dest_Const mC))) $ t')
+ SOME (mC $ Const (\<^const_name>\<open>Groups.one\<close>, domain_type (dest_Const_type mC)) $ t')
| (NONE, NONE) => NONE,
Rat.mult m' (Rat.inv p))
end
--- a/src/HOL/Tools/record.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Tools/record.ML Sun Aug 04 17:39:47 2024 +0200
@@ -989,24 +989,23 @@
fun gen_get_updupd_simps ctxt upd_funs defset =
let
- val cname = fst o dest_Const;
- fun getswap u u' = get_updupd_simp ctxt defset u u' (cname u = cname u');
+ fun getswap u u' = get_updupd_simp ctxt defset u u' (dest_Const_name u = dest_Const_name u');
fun build_swaps_to_eq _ [] swaps = swaps
| build_swaps_to_eq upd (u :: us) swaps =
let
- val key = (cname u, cname upd);
+ val key = (dest_Const_name u, dest_Const_name upd);
val newswaps =
if Symreltab.defined swaps key then swaps
else Symreltab.insert (K true) (key, getswap u upd) swaps;
in
- if cname u = cname upd then newswaps
+ if dest_Const_name u = dest_Const_name upd then newswaps
else build_swaps_to_eq upd us newswaps
end;
fun swaps_needed [] _ _ swaps = map snd (Symreltab.dest swaps)
| swaps_needed (u :: us) prev seen swaps =
- if Symtab.defined seen (cname u)
+ if Symtab.defined seen (dest_Const_name u)
then swaps_needed us prev seen (build_swaps_to_eq u prev swaps)
- else swaps_needed us (u :: prev) (Symtab.insert (K true) (cname u, ()) seen) swaps;
+ else swaps_needed us (u :: prev) (Symtab.insert (K true) (dest_Const_name u, ()) seen) swaps;
in swaps_needed upd_funs [] Symtab.empty Symreltab.empty end;
fun get_updupd_simps ctxt term defset = gen_get_updupd_simps ctxt (get_upd_funs term) defset;
--- a/src/HOL/Tools/typedef.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Tools/typedef.ML Sun Aug 04 17:39:47 2024 +0200
@@ -229,8 +229,8 @@
|> primitive_typedef overloaded type_definition_name newT oldT Rep_name Abs_name set;
val alias_lthy = typedef_lthy
- |> Local_Theory.const_alias Rep_name (#1 (Term.dest_Const RepC))
- |> Local_Theory.const_alias Abs_name (#1 (Term.dest_Const AbsC));
+ |> Local_Theory.const_alias Rep_name (Term.dest_Const_name RepC)
+ |> Local_Theory.const_alias Abs_name (Term.dest_Const_name AbsC);
(* result *)
@@ -272,8 +272,8 @@
make @{thm type_definition.Abs_induct});
val info =
- ({rep_type = oldT, abs_type = newT, Rep_name = #1 (Term.dest_Const RepC),
- Abs_name = #1 (Term.dest_Const AbsC), axiom_name = axiom_name},
+ ({rep_type = oldT, abs_type = newT, Rep_name = dest_Const_name RepC,
+ Abs_name = dest_Const_name AbsC, axiom_name = axiom_name},
{inhabited = inhabited, type_definition = type_definition,
Rep = Rep, Rep_inverse = Rep_inverse, Abs_inverse = Abs_inverse,
Rep_inject = Rep_inject, Abs_inject = Abs_inject, Rep_cases = Rep_cases,
--- a/src/ZF/Datatype.thy Sun Aug 04 16:56:28 2024 +0200
+++ b/src/ZF/Datatype.thy Sun Aug 04 17:39:47 2024 +0200
@@ -86,8 +86,8 @@
val (lhs,rhs) = FOLogic.dest_eq old
val (lhead, largs) = strip_comb lhs
and (rhead, rargs) = strip_comb rhs
- val lname = #1 (dest_Const lhead) handle TERM _ => raise Match;
- val rname = #1 (dest_Const rhead) handle TERM _ => raise Match;
+ val lname = dest_Const_name lhead handle TERM _ => raise Match;
+ val rname = dest_Const_name rhead handle TERM _ => raise Match;
val lcon_info = the (Symtab.lookup (ConstructorsData.get thy) lname)
handle Option.Option => raise Match;
val rcon_info = the (Symtab.lookup (ConstructorsData.get thy) rname)
--- a/src/ZF/Tools/datatype_package.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/ZF/Tools/datatype_package.ML Sun Aug 04 17:39:47 2024 +0200
@@ -55,7 +55,7 @@
error ("Datatype set not previously declared as constant: " ^
Syntax.string_of_term_global \<^theory>\<open>IFOL\<close> t));
val rec_names = (*nat doesn't have to be added*)
- \<^const_name>\<open>nat\<close> :: map (#1 o dest_Const) rec_hds
+ \<^const_name>\<open>nat\<close> :: map dest_Const_name rec_hds
val u = if co then \<^Const>\<open>QUniv.quniv\<close> else \<^Const>\<open>Univ.univ\<close>
val cs = (fold o fold) (fn (_, _, _, prems) => prems |> (fold o fold_aterms)
(fn t as Const (a, _) => if member (op =) rec_names a then I else insert (op =) t
@@ -70,7 +70,7 @@
error ("Datatype set not previously declared as constant: " ^
Syntax.string_of_term_global thy t));
- val rec_names = map (#1 o dest_Const) rec_hds
+ val rec_names = map dest_Const_name rec_hds
val rec_base_names = map Long_Name.base_name rec_names
val big_rec_base_name = space_implode "_" rec_base_names
@@ -384,7 +384,7 @@
|> map Thm.trim_context};
(*associate with each constructor the datatype name and rewrites*)
- val con_pairs = map (fn c => (#1 (dest_Const c), con_info)) constructors
+ val con_pairs = map (fn c => (dest_Const_name c, con_info)) constructors
in
(*Updating theory components: simprules and datatype info*)
--- a/src/ZF/Tools/ind_cases.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/ZF/Tools/ind_cases.ML Sun Aug 04 17:39:47 2024 +0200
@@ -32,8 +32,8 @@
fun err msg = cat_error msg ("Malformed set membership statement: " ^ s);
val A = Syntax.read_prop ctxt s handle ERROR msg => err msg;
- val c = #1 (Term.dest_Const (Term.head_of (#2 (Ind_Syntax.dest_mem (\<^dest_judgment>
- (Logic.strip_imp_concl A)))))) handle TERM _ => err "";
+ val c = dest_Const_name (Term.head_of (#2 (Ind_Syntax.dest_mem (\<^dest_judgment>
+ (Logic.strip_imp_concl A))))) handle TERM _ => err "";
in
(case Symtab.lookup (IndCasesData.get thy) c of
NONE => error ("Unknown inductive cases rule for set " ^ quote c)
--- a/src/ZF/Tools/induct_tacs.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/ZF/Tools/induct_tacs.ML Sun Aug 04 17:39:47 2024 +0200
@@ -68,7 +68,7 @@
exception Find_tname of string
fun find_tname ctxt var As =
- let fun mk_pair \<^Const_>\<open>mem for \<open>Free (v,_)\<close> A\<close> = (v, #1 (dest_Const (head_of A)))
+ let fun mk_pair \<^Const_>\<open>mem for \<open>Free (v,_)\<close> A\<close> = (v, dest_Const_name (head_of A))
| mk_pair _ = raise Match
val pairs = map_filter (try (mk_pair o \<^dest_judgment>)) As
val x =
@@ -151,7 +151,7 @@
|> map Thm.trim_context};
(*associate with each constructor the datatype name and rewrites*)
- val con_pairs = map (fn c => (#1 (dest_Const c), con_info)) constructors
+ val con_pairs = map (fn c => (dest_Const_name c, con_info)) constructors
in
thy
--- a/src/ZF/Tools/inductive_package.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/ZF/Tools/inductive_package.ML Sun Aug 04 17:39:47 2024 +0200
@@ -73,7 +73,7 @@
Syntax.string_of_term ctxt0 t));
(*Now we know they are all Consts, so get their names, type and params*)
- val rec_names = map (#1 o dest_Const) rec_hds
+ val rec_names = map dest_Const_name rec_hds
and (Const(_,recT),rec_params) = strip_comb (hd rec_tms);
val rec_base_names = map Long_Name.base_name rec_names;
@@ -387,7 +387,7 @@
a summand 'domt' was also an argument, but this required the domain of
mutual recursion to invariably be a disjoint sum.*)
fun mk_predpair rec_tm =
- let val rec_name = (#1 o dest_Const o head_of) rec_tm
+ let val rec_name = dest_Const_name (head_of rec_tm)
val pfree = Free(pred_name ^ "_" ^ Long_Name.base_name rec_name,
elem_factors ---> \<^Type>\<open>o\<close>)
val qconcl =
--- a/src/ZF/Tools/primrec_package.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/ZF/Tools/primrec_package.ML Sun Aug 04 17:39:47 2024 +0200
@@ -46,7 +46,7 @@
val (constr, cargs_frees) =
if null middle then raise RecError "constructor missing"
else strip_comb (hd middle);
- val (cname, _) = dest_Const constr
+ val cname = dest_Const_name constr
handle TERM _ => raise RecError "ill-formed constructor";
val con_info = the (Symtab.lookup (ConstructorsData.get thy) cname)
handle Option.Option =>
@@ -102,7 +102,7 @@
fun use_fabs (_ $ t) = subst_bound (t, fabs)
| use_fabs t = t
- val cnames = map (#1 o dest_Const) constructors
+ val cnames = map dest_Const_name constructors
and recursor_pairs = map (dest_eqn o Thm.concl_of) rec_rewrites
fun absterm (Free x, body) = absfree x body