# HG changeset patch # User wenzelm # Date 1722785987 -7200 # Node ID 4041e7c8059d477f67882e96175b7935342a8eff # Parent 27d5452d20fcaee692b9f7fc572d163ddfad886c tuned: more explicit dest_Const_name and dest_Const_type; diff -r 27d5452d20fc -r 4041e7c8059d src/Doc/Eisbach/Base.thy --- 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 _ = diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Data_Structures/Define_Time_Function.ML --- 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 diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Decision_Procs/Conversions.thy --- 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 @@ \convert equality to meta equality\ ML \ -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; diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/HOLCF/Tools/Domain/domain_constructors.ML --- 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 diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/HOLCF/Tools/Domain/domain_induction.ML --- 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 diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/HOLCF/Tools/fixrec.ML --- 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 diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/HOLCF/ex/Pattern_Match.thy --- 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>\Rep_cfun\; val capps = Library.foldl capp diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Hoare/hoare_syntax.ML --- 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 diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Import/import_data.ML --- 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 diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Library/Tools/smt_word.ML --- 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>\nat\ diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Library/adhoc_overloading.ML --- 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 diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Library/case_converter.ML --- 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 diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Library/code_lazy.ML --- 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>\fun\, [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>\fun\, [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, diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Library/conditional_parametricity.ML --- 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) diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Library/datatype_records.ML --- 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 diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Library/old_recdef.ML --- 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; diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/List.thy --- 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 diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Nominal/nominal_inductive.ML --- 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>\Nominal.perm\, _) $ _ $ 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 = []}; diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Nominal/nominal_inductive2.ML --- 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>\Nominal.perm\, _) $ _ $ 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 = []}; diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Real_Asymp/real_asymp.ML --- 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 = diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML --- 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>\All\ then + dest_Const_name t1 = \<^const_name>\All\ 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.*) diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/TPTP/TPTP_Proof_Reconstruction.thy --- 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>\HOL.Ex\) - andalso (get_const_name h <> get_const_name \<^term>\HOL.All\) + andalso (dest_Const_name h <> dest_Const_name \<^term>\HOL.Ex\) + andalso (dest_Const_name h <> dest_Const_name \<^term>\HOL.All\) andalso (h <> \<^term>\Hilbert_Choice.Eps\) andalso (h <> \<^term>\HOL.conj\) andalso (h <> \<^term>\HOL.disj\) @@ -588,11 +587,10 @@ Const (\<^const_name>\HOL.eq\, _) $ t' $ (Const (\<^const_name>\Hilbert_Choice.Eps\, _) $ _) => 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>\HOL.Ex\) - orelse (get_const_name h = get_const_name \<^term>\HOL.All\) + (dest_Const_name h = dest_Const_name \<^term>\HOL.Ex\) + orelse (dest_Const_name h = dest_Const_name \<^term>\HOL.All\) orelse (h = \<^term>\Hilbert_Choice.Eps\) orelse (h = \<^term>\HOL.conj\) orelse (h = \<^term>\HOL.disj\) @@ -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 diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Tools/ATP/atp_util.ML --- 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>\undefined\, 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 = diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Tools/BNF/bnf_def.ML --- 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), diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Tools/BNF/bnf_fp_n2m.ML --- 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 diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Tools/BNF/bnf_fp_util.ML --- 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 => diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Tools/BNF/bnf_gfp.ML --- 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 diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML --- 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_>\Trueprop\ $ (Const (\<^const_name>\HOL.eq\, _) $ _ $ 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}, ...}, diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML --- 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; diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- 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>\case_prod\ then + else if try dest_Const_name u = SOME \<^const_name>\case_prod\ then map (rewrite bound_Ts) vs |> chop 1 |>> HOLogic.mk_case_prod o the_single |> Term.list_comb diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Tools/BNF/bnf_lfp.ML --- 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); diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Tools/BNF/bnf_lfp_compat.ML --- 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}); diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Tools/BNF/bnf_lift.ML --- 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); diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Tools/Ctr_Sugar/case_translation.ML --- 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; diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- 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 diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Tools/Lifting/lifting_def_code_dt.ML --- 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>\id\ then - t else rep $ t + if is_Const rep andalso dest_Const_name rep = \<^const_name>\id\ + then t else rep $ t end; in @{fold 3} (fn sel => fn ctr_T => fn sel_ret_T => fn ctr => diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Tools/Lifting/lifting_info.ML --- 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) diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Tools/Lifting/lifting_setup.ML --- 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 diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Tools/Nitpick/nitpick_hol.ML --- 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>\integer\] 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 diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Tools/Nitpick/nitpick_model.ML --- 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>\nitpick_unrep\, \<^typ>\'a\), mixfix (unrep_mixfix (), [], 1000)) - |>> name_of + |>> dest_Const_name val (maybe_s, thy) = thy |> Sign.declare_const_global ((\<^binding>\nitpick_maybe\, \<^typ>\'a => 'a\), mixfix (maybe_mixfix (), [1000], 1000)) - |>> name_of + |>> dest_Const_name val (abs_s, thy) = thy |> Sign.declare_const_global ((\<^binding>\nitpick_abs\, \<^typ>\'a => 'b\), mixfix (abs_mixfix (), [40], 40)) - |>> name_of + |>> dest_Const_name val (base_s, thy) = thy |> Sign.declare_const_global ((\<^binding>\nitpick_base\, \<^typ>\'a => 'a\), mixfix (base_mixfix (), [1000], 1000)) - |>> name_of + |>> dest_Const_name val (step_s, thy) = thy |> Sign.declare_const_global ((\<^binding>\nitpick_step\, \<^typ>\'a => 'a\), 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) diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Tools/Old_Datatype/old_rep_datatype.ML --- 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 diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Tools/Predicate_Compile/code_prolog.ML --- 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 diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Tools/Predicate_Compile/core_data.ML --- 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 " ^ diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Tools/Predicate_Compile/mode_inference.ML --- 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 diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Tools/Predicate_Compile/predicate_compile.ML --- 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)) diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- 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 = diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- 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 diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML --- 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 diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML --- 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) = diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML --- 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 diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML --- 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 diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Tools/Quotient/quotient_term.ML --- 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.")) diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Tools/SMT/smt_datatypes.ML --- 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)] diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Tools/Transfer/transfer.ML --- 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 diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Tools/Transfer/transfer_bnf.ML --- 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 diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Tools/choice_specification.ML --- 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 = diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Tools/datatype_simprocs.ML --- 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 diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Tools/inductive.ML --- 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 = diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Tools/inductive_realizer.ML --- 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>\Pure.all\, _) $ 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 diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Tools/lin_arith.ML --- 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>\Groups.one\, domain_type (snd (dest_Const mC))) $ t') + SOME (mC $ Const (\<^const_name>\Groups.one\, domain_type (dest_Const_type mC)) $ t') | (NONE, NONE) => NONE, Rat.mult m' (Rat.inv p)) end diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Tools/record.ML --- 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; diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Tools/typedef.ML --- 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, diff -r 27d5452d20fc -r 4041e7c8059d src/ZF/Datatype.thy --- 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) diff -r 27d5452d20fc -r 4041e7c8059d src/ZF/Tools/datatype_package.ML --- 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>\IFOL\ t)); val rec_names = (*nat doesn't have to be added*) - \<^const_name>\nat\ :: map (#1 o dest_Const) rec_hds + \<^const_name>\nat\ :: map dest_Const_name rec_hds val u = if co then \<^Const>\QUniv.quniv\ else \<^Const>\Univ.univ\ 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*) diff -r 27d5452d20fc -r 4041e7c8059d src/ZF/Tools/ind_cases.ML --- 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) diff -r 27d5452d20fc -r 4041e7c8059d src/ZF/Tools/induct_tacs.ML --- 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_>\mem for \Free (v,_)\ A\ = (v, #1 (dest_Const (head_of A))) + let fun mk_pair \<^Const_>\mem for \Free (v,_)\ A\ = (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 diff -r 27d5452d20fc -r 4041e7c8059d src/ZF/Tools/inductive_package.ML --- 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>\o\) val qconcl = diff -r 27d5452d20fc -r 4041e7c8059d src/ZF/Tools/primrec_package.ML --- 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