--- a/src/HOL/HOLCF/Tools/Domain/domain.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain.ML Sun Aug 04 13:24:54 2024 +0200
@@ -182,7 +182,7 @@
fun define_isos (spec : (binding * mixfix * (typ * typ)) list) =
let
fun prep (dbind, mx, (lhsT, rhsT)) =
- let val (_, vs) = dest_Type lhsT
+ let val vs = dest_Type_args lhsT
in (map (fst o dest_TFree) vs, dbind, mx, rhsT, NONE) end
in
Domain_Isomorphism.domain_isomorphism (map prep spec)
--- a/src/HOL/HOLCF/Tools/Domain/domain_axioms.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_axioms.ML Sun Aug 04 13:24:54 2024 +0200
@@ -97,7 +97,7 @@
(* declare new types *)
fun thy_type (dbind, mx, (lhsT, _)) =
- (dbind, (length o snd o dest_Type) lhsT, mx)
+ (dbind, length (dest_Type_args lhsT), mx)
val thy = Sign.add_types_global (map thy_type dom_eqns) thy
(* axiomatize type constructor arities *)
--- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Sun Aug 04 13:24:54 2024 +0200
@@ -930,7 +930,7 @@
let
fun qualified name = Binding.qualify_name true dbind name
val names = "bottom" :: map (fn (b,_,_) => Binding.name_of b) spec
- val dname = fst (dest_Type lhsT)
+ val dname = dest_Type_name lhsT
val simp = Simplifier.simp_add
val case_names = Rule_Cases.case_names names
val cases_type = Induct.cases_type dname
--- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Sun Aug 04 13:24:54 2024 +0200
@@ -212,7 +212,7 @@
in Goal.prove_global thy [] (adms @ assms) goal tacf end
(* case names for induction rules *)
- val dnames = map (fst o dest_Type) newTs
+ val dnames = map dest_Type_name newTs
val case_ns =
let
val adms =
--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Sun Aug 04 13:24:54 2024 +0200
@@ -256,9 +256,9 @@
fun unprime a = Library.unprefix "'" a
fun mapvar T = Free (unprime (fst (dest_TFree T)), T ->> T)
fun map_lhs (map_const, lhsT) =
- (lhsT, list_ccomb (map_const, map mapvar (filter (is_cpo thy) (snd (dest_Type lhsT)))))
+ (lhsT, list_ccomb (map_const, map mapvar (filter (is_cpo thy) (dest_Type_args lhsT))))
val tab1 = map map_lhs (map_consts ~~ map fst dom_eqns)
- val Ts = (snd o dest_Type o fst o hd) dom_eqns
+ val Ts = dest_Type_args (fst (hd dom_eqns))
val tab = (Ts ~~ map mapvar Ts) @ tab1
fun mk_map_spec (((rep_const, abs_const), _), (lhsT, rhsT)) =
let
@@ -285,10 +285,10 @@
fun mk_assm T = mk_trp (mk_deflation (mk_f T))
fun mk_goal (map_const, (lhsT, _)) =
let
- val (_, Ts) = dest_Type lhsT
+ val Ts = dest_Type_args lhsT
val map_term = list_ccomb (map_const, map mk_f (filter (is_cpo thy) Ts))
in mk_deflation map_term end
- val assms = (map mk_assm o filter (is_cpo thy) o snd o dest_Type o fst o hd) dom_eqns
+ val assms = map mk_assm (filter (is_cpo thy) (dest_Type_args (fst (hd dom_eqns))))
val goals = map mk_goal (map_consts ~~ dom_eqns)
val goal = mk_trp (foldr1 HOLogic.mk_conj goals)
val adm_rules =
@@ -329,7 +329,7 @@
local
fun register_map (dname, args) =
Domain_Take_Proofs.add_rec_type (dname, args)
- val dnames = map (fst o dest_Type o fst) dom_eqns
+ val dnames = map (dest_Type_name o fst) dom_eqns
fun args (T, _) = case T of Type (_, Ts) => map (is_cpo thy) Ts | _ => []
val argss = map args dom_eqns
in
@@ -596,7 +596,7 @@
in mk_trp (isodefl_const T $ mk_f T $ mk_d T) end
fun mk_goal (map_const, (T, _)) =
let
- val (_, Ts) = dest_Type T
+ val Ts = dest_Type_args T
val map_term = list_ccomb (map_const, map mk_f (filter (is_cpo thy) Ts))
val defl_term = defl_of_typ thy (Ts ~~ map mk_d Ts) (Ts ~~ map mk_p Ts) T
in isodefl_const T $ map_term $ defl_term end
@@ -645,7 +645,7 @@
fun prove_map_ID_thm
(((map_const, (lhsT, _)), DEFL_thm), isodefl_thm) =
let
- val Ts = snd (dest_Type lhsT)
+ val Ts = dest_Type_args lhsT
fun is_cpo T = Sign.of_sort thy (T, \<^sort>\<open>cpo\<close>)
val lhs = list_ccomb (map_const, map mk_ID (filter is_cpo Ts))
val goal = mk_eqs (lhs, mk_ID lhsT)
@@ -678,7 +678,7 @@
val lhs = mk_tuple (map mk_lub take_consts)
fun is_cpo T = Sign.of_sort thy (T, \<^sort>\<open>cpo\<close>)
fun mk_map_ID (map_const, (lhsT, _)) =
- list_ccomb (map_const, map mk_ID (filter is_cpo (snd (dest_Type lhsT))))
+ list_ccomb (map_const, map mk_ID (filter is_cpo (dest_Type_args lhsT)))
val rhs = mk_tuple (map mk_map_ID (map_consts ~~ dom_eqns))
val goal = mk_trp (mk_eq (lhs, rhs))
val map_ID_thms = Domain_Take_Proofs.get_map_ID_thms thy
--- a/src/HOL/HOLCF/Tools/cpodef.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/HOLCF/Tools/cpodef.ML Sun Aug 04 13:24:54 2024 +0200
@@ -170,7 +170,7 @@
(Typedef.add_typedef {overloaded = false} typ set opt_bindings tac)
val oldT = #rep_type (#1 info)
val newT = #abs_type (#1 info)
- val lhs_tfrees = map dest_TFree (snd (dest_Type newT))
+ val lhs_tfrees = map dest_TFree (dest_Type_args newT)
val RepC = Const (Rep_name, newT --> oldT)
val below_eqn = Logic.mk_equals (below_const newT,
--- a/src/HOL/HOLCF/ex/Pattern_Match.thy Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/HOLCF/ex/Pattern_Match.thy Sun Aug 04 13:24:54 2024 +0200
@@ -461,7 +461,7 @@
(* define pattern combinators *)
local
- val tns = map (fst o dest_TFree) (snd (dest_Type lhsT));
+ val tns = map (fst o dest_TFree) (dest_Type_args lhsT);
fun pat_eqn (i, (bind, (con, args))) : binding * term * mixfix =
let
@@ -527,7 +527,7 @@
(* prove strictness and reduction rules of pattern combinators *)
local
- val tns = map (fst o dest_TFree) (snd (dest_Type lhsT));
+ val tns = map (fst o dest_TFree) (dest_Type_args lhsT);
val rn = singleton (Name.variant_list tns) "'r";
val R = TFree (rn, \<^sort>\<open>pcpo\<close>);
fun pat_lhs (pat, args) =
--- a/src/HOL/Import/import_data.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/Import/import_data.ML Sun Aug 04 13:24:54 2024 +0200
@@ -90,7 +90,7 @@
val (absn, _) = dest_Const abst
val (repn, _) = dest_Const rept
val nty = domain_type (fastype_of rept)
- val ntyn = fst (dest_Type nty)
+ val ntyn = dest_Type_name nty
val thy2 = add_typ_map tyname ntyn thy
val thy3 = add_const_map absname absn thy2
val thy4 = add_const_map repname repn thy3
--- a/src/HOL/Library/case_converter.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/Library/case_converter.ML Sun Aug 04 13:24:54 2024 +0200
@@ -78,7 +78,7 @@
val (ctr, args) = strip_comb term
in
case ctr of Const (s, T) =>
- if P (body_type T |> dest_Type |> fst, s)
+ if P (dest_Type_name (body_type T), s)
then SOME (End (body_type T))
else
let
@@ -103,7 +103,7 @@
val f = hd fs
fun is_single_ctr (Const (name, T)) =
let
- val tyco = body_type T |> dest_Type |> fst
+ val tyco = dest_Type_name (body_type T)
val _ = Ctr_Sugar.ctr_sugar_of ctxt tyco |> the |> #ctrs
in
case Ctr_Sugar.ctr_sugar_of ctxt tyco of
--- a/src/HOL/Library/code_lazy.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/Library/code_lazy.ML Sun Aug 04 13:24:54 2024 +0200
@@ -543,7 +543,7 @@
val table = Laziness_Data.get thy
fun num_consts_fun (_, T) =
let
- val s = body_type T |> dest_Type |> fst
+ val s = dest_Type_name (body_type T)
in
if Symtab.defined table s
then Ctr_Sugar.ctr_sugar_of ctxt s |> the |> #ctrs |> length
--- a/src/HOL/Library/datatype_records.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/Library/datatype_records.ML Sun Aug 04 13:24:54 2024 +0200
@@ -243,11 +243,7 @@
let
val assns = map (apfst (read_const ctxt)) (fields_tr t)
- val typ_name =
- snd (fst (hd assns))
- |> domain_type
- |> dest_Type
- |> fst
+ val typ_name = dest_Type_name (domain_type (snd (fst (hd assns))))
val assns' = map (apfst fst) assns
--- a/src/HOL/Library/refute.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/Library/refute.ML Sun Aug 04 13:24:54 2024 +0200
@@ -2180,7 +2180,7 @@
| Old_Datatype_Aux.DtRec i =>
let
val (_, ds, _) = the (AList.lookup (op =) descr i)
- val (_, Ts) = dest_Type T
+ val Ts = dest_Type_args T
in
rec_typ_assoc ((d, T)::acc) ((ds ~~ Ts) @ xs)
end)
@@ -2195,7 +2195,7 @@
val typ_assoc = filter
(fn (Old_Datatype_Aux.DtTFree _, _) => true | (_, _) => false)
(rec_typ_assoc []
- (#2 (the (AList.lookup (op =) descr idt_index)) ~~ (snd o dest_Type) IDT))
+ (#2 (the (AList.lookup (op =) descr idt_index)) ~~ dest_Type_args IDT))
(* sanity check: typ_assoc must associate types to the *)
(* elements of 'dtyps' (and only to those) *)
val _ =
--- a/src/HOL/Library/simps_case_conv.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/Library/simps_case_conv.ML Sun Aug 04 13:24:54 2024 +0200
@@ -46,7 +46,7 @@
let
fun ctr_count (ctr, T) =
let
- val tyco = body_type T |> dest_Type |> fst
+ val tyco = dest_Type_name (body_type T)
val info = Ctr_Sugar.ctr_sugar_of ctxt tyco
val _ = if is_none info then error ("Pattern match on non-constructor constant " ^ ctr) else ()
in
--- a/src/HOL/List.thy Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/List.thy Sun Aug 04 13:24:54 2024 +0200
@@ -670,7 +670,7 @@
| tac ctxt (Case (T, i) :: cont) =
let
val SOME {injects, distincts, case_thms, split, ...} =
- Ctr_Sugar.ctr_sugar_of ctxt (fst (dest_Type T))
+ Ctr_Sugar.ctr_sugar_of ctxt (dest_Type_name T)
in
(* do case distinction *)
Splitter.split_tac ctxt [split] 1
--- a/src/HOL/Nominal/nominal_datatype.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Sun Aug 04 13:24:54 2024 +0200
@@ -485,7 +485,7 @@
val dt_atomTs = distinct op = (map (Old_Datatype_Aux.typ_of_dtyp descr)
(maps (fn (_, (_, _, cs)) => maps (maps (fst o strip_option) o snd) cs) descr));
- val dt_atoms = map (fst o dest_Type) dt_atomTs;
+ val dt_atoms = map dest_Type_name dt_atomTs;
fun make_intr s T (cname, cargs) =
let
@@ -1578,7 +1578,7 @@
val rec_fin_supp_thms = map (fn aT =>
let
- val name = Long_Name.base_name (fst (dest_Type aT));
+ val name = Long_Name.base_name (dest_Type_name aT);
val fs_name = Global_Theory.get_thm thy11 ("fs_" ^ name ^ "1");
val aset = HOLogic.mk_setT aT;
val finite = Const (\<^const_name>\<open>finite\<close>, aset --> HOLogic.boolT);
@@ -1617,7 +1617,7 @@
val rec_fresh_thms = map (fn ((aT, eqvt_ths), finite_prems) =>
let
- val name = Long_Name.base_name (fst (dest_Type aT));
+ val name = Long_Name.base_name (dest_Type_name aT);
val fs_name = Global_Theory.get_thm thy11 ("fs_" ^ name ^ "1");
val a = Free ("a", aT);
val freshs = map (fn (f, fT) => HOLogic.mk_Trueprop
--- a/src/HOL/Nominal/nominal_inductive.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Sun Aug 04 13:24:54 2024 +0200
@@ -204,7 +204,7 @@
val atomTs = distinct op = (maps (map snd o #2) prems);
val ind_sort = if null atomTs then \<^sort>\<open>type\<close>
else Sign.minimize_sort thy (Sign.certify_sort thy (map (fn T => Sign.intern_class thy
- ("fs_" ^ Long_Name.base_name (fst (dest_Type T)))) atomTs));
+ ("fs_" ^ Long_Name.base_name (dest_Type_name T))) atomTs));
val (fs_ctxt_tyname, _) = Name.variant "'n" (Variable.names_of ctxt');
val ([fs_ctxt_name], ctxt'') = Variable.variant_fixes ["z"] ctxt';
val fsT = TFree (fs_ctxt_tyname, ind_sort);
@@ -276,7 +276,7 @@
val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp";
val pt2_atoms = map (fn aT => Global_Theory.get_thm thy
- ("pt_" ^ Long_Name.base_name (fst (dest_Type aT)) ^ "2")) atomTs;
+ ("pt_" ^ Long_Name.base_name (dest_Type_name aT) ^ "2")) atomTs;
fun eqvt_ss ctxt =
put_simpset HOL_basic_ss ctxt
addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
@@ -285,7 +285,7 @@
val fresh_bij = Global_Theory.get_thms thy "fresh_bij";
val perm_bij = Global_Theory.get_thms thy "perm_bij";
val fs_atoms = map (fn aT => Global_Theory.get_thm thy
- ("fs_" ^ Long_Name.base_name (fst (dest_Type aT)) ^ "1")) atomTs;
+ ("fs_" ^ Long_Name.base_name (dest_Type_name aT) ^ "1")) atomTs;
val exists_fresh' = Global_Theory.get_thms thy "exists_fresh'";
val fresh_atm = Global_Theory.get_thms thy "fresh_atm";
val swap_simps = Global_Theory.get_thms thy "swap_simps";
--- a/src/HOL/Nominal/nominal_inductive2.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML Sun Aug 04 13:24:54 2024 +0200
@@ -227,7 +227,7 @@
end) (Logic.strip_imp_prems raw_induct' ~~ induct_cases');
val atomTs = distinct op = (maps (map snd o #2) prems);
- val atoms = map (fst o dest_Type) atomTs;
+ val atoms = map dest_Type_name atomTs;
val ind_sort = if null atomTs then \<^sort>\<open>type\<close>
else Sign.minimize_sort thy (Sign.certify_sort thy (map (fn a => Sign.intern_class thy
("fs_" ^ Long_Name.base_name a)) atoms));
@@ -321,7 +321,7 @@
fun protect t =
let val T = fastype_of t in Const (\<^const_name>\<open>Fun.id\<close>, T --> T) $ t end;
val p = foldr1 HOLogic.mk_prod (map protect ts);
- val atom = fst (dest_Type T);
+ val atom = dest_Type_name T;
val {at_inst, ...} = NominalAtoms.the_atom_info thy atom;
val fs_atom = Global_Theory.get_thm thy
("fs_" ^ Long_Name.base_name atom ^ "1");
--- a/src/HOL/Nominal/nominal_primrec.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML Sun Aug 04 13:24:54 2024 +0200
@@ -58,7 +58,7 @@
else strip_comb (hd middle);
val (cname, T) = dest_Const constr
handle TERM _ => raise RecError "ill-formed constructor";
- val (tname, _) = dest_Type (body_type T) handle TYPE _ =>
+ val tname = dest_Type_name (body_type T) handle TYPE _ =>
raise RecError "cannot determine datatype associated with function"
val (ls, cargs, rs) =
--- a/src/HOL/Quickcheck_Examples/Quickcheck_Nesting.thy Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Nesting.thy Sun Aug 04 13:24:54 2024 +0200
@@ -10,7 +10,7 @@
val compat_plugin = Plugin_Name.declare_setup \<^binding>\<open>compat\<close>;
fun compat fp_sugars =
- perhaps (try (datatype_compat (map (fst o dest_Type o #T) fp_sugars)));
+ perhaps (try (datatype_compat (map (dest_Type_name o #T) fp_sugars)));
in
Theory.setup (fp_sugars_interpretation compat_plugin compat)
end
--- a/src/HOL/Statespace/distinct_tree_prover.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/Statespace/distinct_tree_prover.ML Sun Aug 04 13:24:54 2024 +0200
@@ -307,7 +307,7 @@
fun subtractProver ctxt (Const (\<^const_name>\<open>Tip\<close>, T)) ct dist_thm =
let
val ct' = dist_thm |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
- val [alphaI] = #2 (dest_Type T);
+ val [alphaI] = dest_Type_args T;
in
Thm.instantiate
(TVars.make1 (alpha, Thm.ctyp_of ctxt alphaI),
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Sun Aug 04 13:24:54 2024 +0200
@@ -2271,7 +2271,7 @@
Formula ((tcon_clause_prefix ^ name, ""), Axiom,
mk_ahorn (maps (class_atoms type_enc) prems)
(class_atom type_enc (cl, T))
- |> bound_tvars type_enc true (snd (dest_Type T)),
+ |> bound_tvars type_enc true (dest_Type_args T),
NONE, isabelle_info generate_isabelle_info inductiveN helper_rank)
fun line_of_conjecture ctxt mono type_enc ({name, role, iformula, atomic_types, ...} : ifact) =
--- a/src/HOL/Tools/BNF/bnf_comp.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/Tools/BNF/bnf_comp.ML Sun Aug 04 13:24:54 2024 +0200
@@ -817,7 +817,7 @@
fun mk_abs_or_rep _ absU (Const (\<^const_name>\<open>id_bnf\<close>, _)) =
Const (\<^const_name>\<open>id_bnf\<close>, absU --> absU)
| mk_abs_or_rep getT (Type (_, Us)) abs =
- let val Ts = snd (dest_Type (getT (fastype_of abs)))
+ let val Ts = dest_Type_args (getT (fastype_of abs))
in Term.subst_atomic_types (Ts ~~ Us) abs end;
val mk_abs = mk_abs_or_rep range_type;
@@ -993,7 +993,7 @@
val (noted, lthy'') = lthy'
|> Local_Theory.notes notes
- ||> (if repTA = TA then I else register_bnf_raw (fst (dest_Type TA)) bnf'')
+ ||> (if repTA = TA then I else register_bnf_raw (dest_Type_name TA) bnf'')
in
((morph_bnf (substitute_noted_thm noted) bnf'', (all_deads, absT_info)), lthy'')
end;
@@ -1037,7 +1037,7 @@
val odead = dead_of_bnf bnf;
val olive = live_of_bnf bnf;
val Ds = map (fn i => TFree (string_of_int i, [])) (1 upto odead);
- val Us = snd (Term.dest_Type (mk_T_of_bnf Ds (replicate olive dummyT) bnf));
+ val Us = Term.dest_Type_args (mk_T_of_bnf Ds (replicate olive dummyT) bnf);
val oDs_pos = map (fn x => find_index (fn y => x = y) Us) Ds
|> filter (fn x => x >= 0);
val oDs = map (nth Ts) oDs_pos;
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Sun Aug 04 13:24:54 2024 +0200
@@ -2694,7 +2694,7 @@
|> Local_Theory.notes (common_notes @ notes)
(* for "datatype_realizer.ML": *)
|>> name_noted_thms
- (fst (dest_Type (hd fpTs)) ^ implode (map (prefix "_") (tl fp_b_names))) inductN
+ (dest_Type_name (hd fpTs) ^ implode (map (prefix "_") (tl fp_b_names))) inductN
|-> interpret_bnfs_register_fp_sugars plugins fpTs fpBTs Xs Least_FP pre_bnfs absT_infos
fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctor_iff_dtors ctr_defss ctr_sugars
recs rec_defs map_thmss [induct_thm] (map single induct_thms) rec_thmss (replicate nn [])
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Sun Aug 04 13:24:54 2024 +0200
@@ -499,7 +499,7 @@
val perm_callers = permute callers;
val perm_kks = permute kks;
val perm_callssss0 = permute callssss0;
- val perm_fp_sugars0 = map (the o fp_sugar_of lthy o fst o dest_Type) perm_Ts;
+ val perm_fp_sugars0 = map (the o fp_sugar_of lthy o dest_Type_name) perm_Ts;
val perm_callssss =
map2 (indexify_callsss o #ctrs o #ctr_sugar o #fp_ctr_sugar) perm_fp_sugars0 perm_callssss0;
--- a/src/HOL/Tools/BNF/bnf_gfp_grec.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML Sun Aug 04 13:24:54 2024 +0200
@@ -2114,8 +2114,8 @@
val sig_ctr_sugar = #ctr_sugar sig_fp_ctr_sugar;
val ssig_ctr_sugar = #ctr_sugar ssig_fp_ctr_sugar;
- val sig_T_name = fst (dest_Type (#T sig_fp_sugar));
- val ssig_T_name = fst (dest_Type (#T ssig_fp_sugar));
+ val sig_T_name = dest_Type_name (#T sig_fp_sugar);
+ val ssig_T_name = dest_Type_name (#T ssig_fp_sugar);
val sig_T = Type (sig_T_name, As);
val ssig_T = Type (ssig_T_name, As);
@@ -2337,10 +2337,10 @@
val sig_ctr_sugar = #ctr_sugar sig_fp_ctr_sugar;
val ssig_ctr_sugar = #ctr_sugar ssig_fp_ctr_sugar;
- val old_sig_T_name = fst (dest_Type (#T old_sig_fp_sugar));
- val old_ssig_T_name = fst (dest_Type (#T old_ssig_fp_sugar));
- val sig_T_name = fst (dest_Type (#T sig_fp_sugar));
- val ssig_T_name = fst (dest_Type (#T ssig_fp_sugar));
+ val old_sig_T_name = dest_Type_name (#T old_sig_fp_sugar);
+ val old_ssig_T_name = dest_Type_name (#T old_ssig_fp_sugar);
+ val sig_T_name = dest_Type_name (#T sig_fp_sugar);
+ val ssig_T_name = dest_Type_name (#T ssig_fp_sugar);
val res_As = res_Ds @ [Y];
val res_Bs = res_Ds @ [Z];
@@ -2618,10 +2618,10 @@
val ctor = mk_ctor res_Ds (the_single (#ctors fp_res));
val dtor = mk_dtor res_Ds (the_single (#dtors fp_res));
- val old1_sig_T_name = fst (dest_Type (#T old1_sig_fp_sugar));
- val old2_sig_T_name = fst (dest_Type (#T old2_sig_fp_sugar));
- val old1_ssig_T_name = fst (dest_Type (#T old1_ssig_fp_sugar));
- val old2_ssig_T_name = fst (dest_Type (#T old2_ssig_fp_sugar));
+ val old1_sig_T_name = dest_Type_name (#T old1_sig_fp_sugar);
+ val old2_sig_T_name = dest_Type_name (#T old2_sig_fp_sugar);
+ val old1_ssig_T_name = dest_Type_name (#T old1_ssig_fp_sugar);
+ val old2_ssig_T_name = dest_Type_name (#T old2_ssig_fp_sugar);
val fp_alives = map (K false) live_fp_alives;
@@ -2648,8 +2648,8 @@
|> define_sig_type fp_b version fp_alives Ds Y (mk_sumT (old1_sig_T0, old2_sig_T0))
||>> define_ssig_type fp_b version fp_alives Ds Y fpT0;
- val sig_T_name = fst (dest_Type (#T sig_fp_sugar));
- val ssig_T_name = fst (dest_Type (#T ssig_fp_sugar));
+ val sig_T_name = dest_Type_name (#T sig_fp_sugar);
+ val ssig_T_name = dest_Type_name (#T ssig_fp_sugar);
val old1_sig_bnf = #fp_bnf old1_sig_fp_sugar;
val old2_sig_bnf = #fp_bnf old2_sig_fp_sugar;
@@ -2848,7 +2848,7 @@
Symtab.map (K (apsnd embed_Sig_inr)) (#friends old2_buffer));
val old_fp_sugars =
- merge_lists (op = o apply2 (fst o dest_Type o #T)) old1_sig_fp_sugars old2_sig_fp_sugars;
+ merge_lists (op = o apply2 (dest_Type_name o #T)) old1_sig_fp_sugars old2_sig_fp_sugars;
val ((dtor_coinduct_info, all_dead_k_bnfs, friend_names), lthy) = lthy
|> derive_cong_merge fp_b version fpT old1_friend_names old2_friend_names dead_ssig_bnf
@@ -3078,7 +3078,7 @@
val (old_info as {friend_names = old_friend_names, sig_fp_sugars = old_sig_fp_sugar :: _,
buffer = old_buffer, ...}, lthy) =
corec_info_of res_T lthy;
- val old_sig_T_name = fst (dest_Type (#T old_sig_fp_sugar));
+ val old_sig_T_name = dest_Type_name (#T old_sig_fp_sugar);
val old_sig_alives = liveness_of_fp_bnf (num_fp_tyargs + 1) (#fp_bnf old_sig_fp_sugar);
(* FIXME: later *)
@@ -3137,7 +3137,7 @@
val sig_ctr_sugar = #ctr_sugar sig_fp_ctr_sugar;
val ssig_ctr_sugar = #ctr_sugar ssig_fp_ctr_sugar;
- val ssig_T_name = fst (dest_Type (#T ssig_fp_sugar));
+ val ssig_T_name = dest_Type_name (#T ssig_fp_sugar);
val preT = pre_type_of_ctor Y ctor;
val old_sig_T = substDT old_sig_T0;
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Sun Aug 04 13:24:54 2024 +0200
@@ -332,7 +332,7 @@
val fp_map_ident = map_ident_of_bnf fp_bnf;
val fpsig_nesting_bnfs = fp_nesting_bnfs @ maps #live_nesting_bnfs sig_fp_sugars;
- val fpsig_nesting_T_names = map (fst o dest_Type o T_of_bnf) fpsig_nesting_bnfs;
+ val fpsig_nesting_T_names = map (dest_Type_name o T_of_bnf) fpsig_nesting_bnfs;
val fpsig_nesting_fp_sugars = map_filter (fp_sugar_of ctxt) fpsig_nesting_T_names;
val fpsig_nesting_fp_bnf_sugars = map #fp_bnf_sugar fpsig_nesting_fp_sugars;
val ssig_fp_bnf_sugar = #fp_bnf_sugar ssig_fp_sugar;
@@ -373,7 +373,7 @@
val fp_map_ident = map_ident_of_bnf fp_bnf;
val fpsig_nesting_bnfs = fp_nesting_bnfs @ maps #live_nesting_bnfs sig_fp_sugars;
- val fpsig_nesting_T_names = map (fst o dest_Type o T_of_bnf) fpsig_nesting_bnfs;
+ val fpsig_nesting_T_names = map (dest_Type_name o T_of_bnf) fpsig_nesting_bnfs;
val fpsig_nesting_fp_sugars = map_filter (fp_sugar_of ctxt) fpsig_nesting_T_names;
val fpsig_nesting_fp_bnf_sugars = map #fp_bnf_sugar fpsig_nesting_fp_sugars;
val ssig_fp_bnf_sugar = #fp_bnf_sugar ssig_fp_sugar;
@@ -492,7 +492,7 @@
val fp_map_ident = map_ident_of_bnf fp_bnf;
val fpsig_nesting_bnfs = fp_nesting_bnfs @ maps #live_nesting_bnfs sig_fp_sugars;
- val fpsig_nesting_T_names = map (fst o dest_Type o T_of_bnf) fpsig_nesting_bnfs;
+ val fpsig_nesting_T_names = map (dest_Type_name o T_of_bnf) fpsig_nesting_bnfs;
val fpsig_nesting_fp_sugars = map_filter (fp_sugar_of ctxt) fpsig_nesting_T_names;
val fpsig_nesting_fp_bnf_sugars = map #fp_bnf_sugar fpsig_nesting_fp_sugars;
val ssig_fp_bnf_sugar = #fp_bnf_sugar ssig_fp_sugar;
@@ -986,7 +986,7 @@
fun has_res_T bound_Ts t = fastype_of1 (bound_Ts, t) = res_T;
- fun contains_res_T (Type (s, Ts)) = s = fst (dest_Type res_T) orelse exists contains_res_T Ts
+ fun contains_res_T (Type (s, Ts)) = s = dest_Type_name res_T orelse exists contains_res_T Ts
| contains_res_T _ = false;
val res_T_lhs_args = filter (exists_type contains_res_T) lhs_args;
@@ -1217,7 +1217,7 @@
((fun_t, arg :: []), true) =>
let val arg_T = fastype_of1 (bound_Ts, arg) in
if arg_T <> res_T then
- (case arg_T |> try (fst o dest_Type) |> Option.mapPartial (ctr_sugar_of lthy) of
+ (case arg_T |> try dest_Type_name |> Option.mapPartial (ctr_sugar_of lthy) of
SOME {discs, T = Type (_, Ts), ...} =>
(case const_of discs fun_t of
SOME disc =>
@@ -1241,7 +1241,7 @@
explore params t
else
let val T = fastype_of1 (bound_Ts, hd args) in
- (case (Option.mapPartial (ctr_sugar_of lthy) (try (fst o dest_Type) T), T <> res_T) of
+ (case (Option.mapPartial (ctr_sugar_of lthy) (try dest_Type_name T), T <> res_T) of
(SOME {selss, T = Type (_, Ts), ...}, true) =>
(case const_of (flat selss) fun_t of
SOME sel =>
@@ -1486,7 +1486,7 @@
error (quote (Syntax.string_of_term lthy (hd obj_leftovers)) ^
" is not a valid case argument");
- val Us = obj_leftoverUs |> hd |> dest_Type |> snd;
+ val Us = dest_Type_args (hd obj_leftoverUs);
val branche_binderUss =
(if hd obj_leftoverUs = YpreT then mk_case HOLogic.boolT
@@ -1895,7 +1895,7 @@
val fp_map_ident = map_ident_of_bnf fp_bnf;
val fpsig_nesting_bnfs = fp_nesting_bnfs @ maps #live_nesting_bnfs sig_fp_sugars;
- val fpsig_nesting_T_names = map (fst o dest_Type o T_of_bnf) fpsig_nesting_bnfs;
+ val fpsig_nesting_T_names = map (dest_Type_name o T_of_bnf) fpsig_nesting_bnfs;
val fpsig_nesting_fp_sugars = map_filter (fp_sugar_of ctxt) fpsig_nesting_T_names;
val fpsig_nesting_fp_bnf_sugars = map #fp_bnf_sugar fpsig_nesting_fp_sugars;
val ssig_fp_bnf_sugar = #fp_bnf_sugar ssig_fp_sugar;
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Sun Aug 04 13:24:54 2024 +0200
@@ -1059,7 +1059,7 @@
let
val (bs, mxs) = map_split (apfst fst) fixes;
val (arg_Ts, res_Ts) = map (strip_type o snd o fst #>> mk_tupleT_balanced) fixes |> split_list;
- val primcorec_types = map (#1 o dest_Type) res_Ts;
+ val primcorec_types = map dest_Type_name res_Ts;
val _ = check_duplicate_const_names bs;
val _ = List.app (uncurry (check_top_sort lthy)) (bs ~~ arg_Ts);
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Sun Aug 04 13:24:54 2024 +0200
@@ -221,9 +221,9 @@
| _ => not_datatype_name s);
val fpTs0 as Type (_, var_As) :: _ =
- map (#T o checked_fp_sugar_of o fst o dest_Type)
+ map (#T o checked_fp_sugar_of o dest_Type_name)
(#Ts (#fp_res (checked_fp_sugar_of (hd fpT_names0))));
- val fpT_names as fpT_name1 :: _ = map (fst o dest_Type) fpTs0;
+ val fpT_names as fpT_name1 :: _ = map (dest_Type_name) fpTs0;
val _ = check_names (op =) (fpT_names0, fpT_names) orelse not_mutually_recursive fpT_names0;
@@ -272,7 +272,7 @@
val fpTs' = Old_Datatype_Aux.get_rec_types descr;
val nn = length fpTs';
- val fp_sugars = map (checked_fp_sugar_of o fst o dest_Type) fpTs';
+ val fp_sugars = map (checked_fp_sugar_of o dest_Type_name) fpTs';
val ctr_Tsss = map (map (map (Old_Datatype_Aux.typ_of_dtyp descr) o snd) o #3 o snd) descr;
val kkssss = map (map (map body_rec_indices o snd) o #3 o snd) descr;
@@ -447,7 +447,7 @@
thy;
fun new_interpretation_of prefs f (fp_sugars : fp_sugar list) thy =
- let val T_names = map (fst o dest_Type o #T) fp_sugars in
+ let val T_names = map (dest_Type_name o #T) fp_sugars in
if (member (op =) prefs Include_GFPs orelse forall (curry (op =) Least_FP o #fp) fp_sugars)
andalso (member (op =) prefs Keep_Nesting orelse
exists (is_none o Old_Datatype_Data.get_info thy) T_names) then
@@ -511,7 +511,7 @@
fun datatype_compat_cmd raw_fpT_names lthy =
let
val fpT_names =
- map (fst o dest_Type o Proof_Context.read_type_name {proper = true, strict = false} lthy)
+ map (dest_Type_name o Proof_Context.read_type_name {proper = true, strict = false} lthy)
raw_fpT_names;
in
datatype_compat fpT_names lthy
--- a/src/HOL/Tools/BNF/bnf_lfp_countable.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_countable.ML Sun Aug 04 13:24:54 2024 +0200
@@ -137,8 +137,8 @@
| _ => not_datatype_name s);
val fpTs0 as Type (_, var_As) :: _ =
- map (#T o lfp_sugar_of o fst o dest_Type) (#Ts (#fp_res (lfp_sugar_of (hd fpT_names0))));
- val fpT_names = map (fst o dest_Type) fpTs0;
+ map (#T o lfp_sugar_of o dest_Type_name) (#Ts (#fp_res (lfp_sugar_of (hd fpT_names0))));
+ val fpT_names = map dest_Type_name fpTs0;
val (As_names, _) = Variable.variant_fixes (map (fn TVar ((s, _), _) => s) var_As) ctxt;
val As =
@@ -156,7 +156,7 @@
val fp_sugars as
{fp_nesting_bnfs, fp_co_induct_sugar = SOME {common_co_inducts = induct :: _, ...},
...} :: _ =
- map (the o fp_sugar_of ctxt o fst o dest_Type) fpTs0;
+ map (the o fp_sugar_of ctxt o dest_Type_name) fpTs0;
val ctr_sugars = map (#ctr_sugar o #fp_ctr_sugar) fp_sugars;
val ctrss0 = map #ctrs ctr_sugars;
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Sun Aug 04 13:24:54 2024 +0200
@@ -615,7 +615,7 @@
val ((jss, simpss), lthy) = prove lthy defs;
val res =
{prefix = (names, qualifys),
- types = map (#1 o dest_Type) arg_Ts,
+ types = map dest_Type_name arg_Ts,
result = (map fst defs, map (snd o snd) defs, (jss, simpss))};
in (res, lthy) end)
end;
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Sun Aug 04 13:24:54 2024 +0200
@@ -103,7 +103,7 @@
val data = Data.get (Context.Proof lthy0);
val Ts = map #T fp_sugars
- val T_names = map (fst o dest_Type) Ts;
+ val T_names = map dest_Type_name Ts;
val nn = length Ts;
val B_ify = Term.typ_subst_atomic (As ~~ Bs);
--- a/src/HOL/Tools/BNF/bnf_lift.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/Tools/BNF/bnf_lift.ML Sun Aug 04 13:24:54 2024 +0200
@@ -411,8 +411,8 @@
val typ_Abs_G = dest_funT (fastype_of Abs_G);
val RepT = fst typ_Abs_G; (* F *)
val AbsT = snd typ_Abs_G; (* G *)
- val AbsT_name = fst (dest_Type AbsT);
- val tvs = AbsT |> dest_Type |> snd |> map (fst o dest_TVar);
+ val AbsT_name = dest_Type_name AbsT;
+ val tvs = AbsT |> dest_Type_args |> map (fst o dest_TVar);
val alpha0s = map (TFree o snd) specs;
val _ = length tvs = length alpha0s orelse
@@ -833,9 +833,9 @@
(* extract rep_G and abs_G *)
val (equiv_rel, abs_G, rep_G) = strip3 quot_thm;
val (repT, absT) = dest_funT (fastype_of abs_G); (* ("?'a F", "?'a G") *)
- val absT_name = fst (dest_Type absT);
+ val absT_name = dest_Type_name absT;
- val tvs = map (fst o dest_TVar) (snd (dest_Type absT));
+ val tvs = map (fst o dest_TVar) (dest_Type_args absT);
val _ = length tvs = length specs orelse
error ("Expected " ^ string_of_int (length tvs) ^
" type argument" ^ (if (length tvs) = 1 then "" else "s") ^ " to " ^ quote absT_name);
@@ -2052,7 +2052,7 @@
val lift_bnf_cmd =
prepare_lift_bnf
- (fst o dest_Type oo Proof_Context.read_type_name {proper = true, strict = false})
+ (dest_Type_name oo Proof_Context.read_type_name {proper = true, strict = false})
Syntax.read_sort Syntax.read_term Attrib.eval_thms;
fun lift_bnf args tacs =
@@ -2071,7 +2071,7 @@
apfst (apfst (rpair NONE))
#> apfst (apsnd (Option.map single))
#> prepare_solve
- (fst o dest_Type oo Proof_Context.read_type_name {proper = true, strict = false})
+ (dest_Type_name oo Proof_Context.read_type_name {proper = true, strict = false})
Syntax.read_sort Syntax.read_term Attrib.eval_thms
(fn n => replicate n copy_bnf_tac);
--- a/src/HOL/Tools/Ctr_Sugar/case_translation.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/case_translation.ML Sun Aug 04 13:24:54 2024 +0200
@@ -85,7 +85,7 @@
|> funpow (length constrs) range_type
|> domain_type;
-val Tname_of_data = fst o dest_Type o T_of_data;
+val Tname_of_data = dest_Type_name o T_of_data;
val constrs_of = #constrs o rep_data;
val cases_of = #cases o rep_data;
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Sun Aug 04 13:24:54 2024 +0200
@@ -296,7 +296,7 @@
end;
fun mk_disc_or_sel Ts t =
- subst_nonatomic_types (snd (Term.dest_Type (domain_type (fastype_of t))) ~~ Ts) t;
+ subst_nonatomic_types (Term.dest_Type_args (domain_type (fastype_of t)) ~~ Ts) t;
val name_of_ctr = name_of_const "constructor" body_type;
--- a/src/HOL/Tools/Function/function_elims.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/Tools/Function/function_elims.ML Sun Aug 04 13:24:54 2024 +0200
@@ -109,7 +109,7 @@
val (rhs_var, arg_vars, prop) = mk_funeq arity (fastype_of f) ([], f);
val args = HOLogic.mk_tuple arg_vars;
- val domT = R |> dest_Free |> snd |> hd o snd o dest_Type;
+ val domT = hd (dest_Type_args (snd (dest_Free R)));
val P = Thm.cterm_of ctxt (variant_free prop ("P", \<^typ>\<open>bool\<close>));
val sumtree_inj = Sum_Tree.mk_inj domT n_fs (idx + 1) args;
--- a/src/HOL/Tools/Lifting/lifting_bnf.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/Tools/Lifting/lifting_bnf.ML Sun Aug 04 13:24:54 2024 +0200
@@ -22,7 +22,7 @@
val rel_Grp = rel_Grp_of_bnf bnf
fun get_lhs thm = thm |> Thm.concl_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> fst
val vars = get_lhs rel_Grp |> strip_comb |> snd |> map_filter (try (strip_comb #> snd #> hd))
- val UNIVs = map (fn var => HOLogic.mk_UNIV (var |> dest_Var |> snd |> dest_Type |> snd |> hd)) vars
+ val UNIVs = map (fn var => HOLogic.mk_UNIV (var |> dest_Var |> snd |> dest_Type_args |> hd)) vars
val inst = map dest_Var vars ~~ map (Thm.cterm_of ctxt) UNIVs
val rel_Grp_UNIV_sym = rel_Grp |> Drule.instantiate_normalize (TVars.empty, Vars.make inst)
|> Local_Defs.unfold0 ctxt @{thms subset_UNIV[THEN eqTrueI] UNIV_def[symmetric] simp_thms(21)}
--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Sun Aug 04 13:24:54 2024 +0200
@@ -353,7 +353,7 @@
(* in order to make the qty qty_isom isomorphism executable we have to define discriminators
and selectors for qty_isom *)
val (rty_name, typs) = dest_Type rty
- val (_, qty_typs) = dest_Type qty
+ val qty_typs = dest_Type_args qty
val fp = BNF_FP_Def_Sugar.fp_sugar_of lthy3 rty_name
val fp = if is_some fp then the fp
else error ("code_dt: " ^ quote rty_name ^ " is not a datatype.")
--- a/src/HOL/Tools/Lifting/lifting_info.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/Tools/Lifting/lifting_info.ML Sun Aug 04 13:24:54 2024 +0200
@@ -184,7 +184,7 @@
val _ = Context.cases (K ()) (quot_map_thm_sanity_check rel_quot_thm) context
val rel_quot_thm_concl = Logic.strip_imp_concl (Thm.prop_of rel_quot_thm)
val (_, abs, _, _) = dest_Quotient (HOLogic.dest_Trueprop rel_quot_thm_concl)
- val relatorT_name = fst (dest_Type (fst (dest_funT (fastype_of abs))))
+ val relatorT_name = dest_Type_name (fst (dest_funT (fastype_of abs)))
val minfo = {rel_quot_thm = Thm.trim_context rel_quot_thm}
in (Data.map o map_quot_maps) (Symtab.update (relatorT_name, minfo)) context end
@@ -223,7 +223,7 @@
fun lookup_quot_thm_quotients ctxt quot_thm =
let
val (_, qtyp) = quot_thm_rty_qty quot_thm
- val qty_full_name = fst (dest_Type qtyp)
+ val qty_full_name = dest_Type_name qtyp
fun compare_data (data:quotient) = Thm.eq_thm_prop (#quot_thm data, quot_thm)
in
case lookup_quotients ctxt qty_full_name of
@@ -238,7 +238,7 @@
fun delete_quotients quot_thm context =
let
val (_, qtyp) = quot_thm_rty_qty quot_thm
- val qty_full_name = fst (dest_Type qtyp)
+ val qty_full_name = dest_Type_name qtyp
in
if is_some (lookup_quot_thm_quotients (Context.proof_of context) quot_thm)
then (Data.map o map_quotients) (Symtab.delete qty_full_name) context
@@ -391,8 +391,8 @@
let
val pol_mono_rule = introduce_polarities mono_rule
val mono_ruleT_name =
- fst (dest_Type (fst (relation_types (fst (relation_types
- (snd (dest_Const (head_of (HOLogic.dest_Trueprop (Thm.concl_of pol_mono_rule))))))))))
+ dest_Type_name (fst (relation_types (fst (relation_types
+ (snd (dest_Const (head_of (HOLogic.dest_Trueprop (Thm.concl_of pol_mono_rule)))))))))
in
if Symtab.defined (get_relator_distr_data' context) mono_ruleT_name
then
@@ -418,8 +418,8 @@
fun add_distr_rule update_entry distr_rule context =
let
val distr_ruleT_name =
- fst (dest_Type (fst (relation_types (fst (relation_types
- (snd (dest_Const (head_of (HOLogic.dest_Trueprop (Thm.concl_of distr_rule))))))))))
+ dest_Type_name (fst (relation_types (fst (relation_types
+ (snd (dest_Const (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 13:14:33 2024 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Sun Aug 04 13:24:54 2024 +0200
@@ -42,7 +42,7 @@
val (qty, rty) = (dest_funT o fastype_of) rep_fun
val rep_fun_graph = (HOLogic.eq_const rty) $ Bound 1 $ (rep_fun $ Bound 0)
val def_term = Abs ("x", rty, Abs ("y", qty, rep_fun_graph))
- val qty_name = (Binding.name o Long_Name.base_name o fst o dest_Type) qty
+ val qty_name = Binding.name (Long_Name.base_name (dest_Type_name qty))
val crel_name = Binding.prefix_name "cr_" qty_name
val (fixed_def_term, lthy1) = lthy |> yield_singleton (Variable.importT_terms) def_term
val ((_, (_ , def_thm)), lthy2) =
@@ -85,7 +85,7 @@
(rty --> rty' --> HOLogic.boolT) -->
(rty' --> qty --> HOLogic.boolT) -->
rty --> qty --> HOLogic.boolT)
- val qty_name = (fst o dest_Type) qty
+ val qty_name = dest_Type_name qty
val pcrel_name = Binding.prefix_name "pcr_" ((Binding.name o Long_Name.base_name) qty_name)
val relator_type = foldr1 (op -->) ((map type_of args_fixed) @ [rty, qty, HOLogic.boolT])
val lhs = Library.foldl (op $) ((Free (Binding.name_of pcrel_name, relator_type)), args_fixed)
@@ -131,8 +131,8 @@
let
val lhs = (Thm.term_of o Thm.lhs_of) pcr_rel_def
val qty_name =
- (Binding.name o Long_Name.base_name o fst o dest_Type o
- List.last o binder_types o fastype_of) lhs
+ Binding.name
+ (Long_Name.base_name (dest_Type_name (List.last (binder_types (fastype_of lhs)))))
val args = (snd o strip_comb) lhs
fun make_inst var ctxt =
@@ -270,7 +270,7 @@
SOME pcrel_def => SOME { pcrel_def = pcrel_def, pcr_cr_eq = the pcr_cr_eq }
| NONE => NONE
val quotients = { quot_thm = quot_thm, pcr_info = pcr_info }
- val qty_full_name = (fst o dest_Type) qty
+ val qty_full_name = dest_Type_name qty
fun quot_info phi = Lifting_Info.transform_quotient phi quotients
val reflexivity_rule_attr = Attrib.internal \<^here> (K Lifting_Info.add_reflexivity_rule_attribute)
val lthy3 =
@@ -520,9 +520,9 @@
val quot_thm = Morphism.thm (Local_Theory.target_morphism lthy0) quot_thm
(**)
val (rty, qty) = quot_thm_rty_qty quot_thm
- val induct_attr = Attrib.internal \<^here> (K (Induct.induct_type (fst (dest_Type qty))))
- val qty_full_name = (fst o dest_Type) qty
- val qty_name = (Binding.name o Long_Name.base_name) qty_full_name
+ val induct_attr = Attrib.internal \<^here> (K (Induct.induct_type (dest_Type_name qty)))
+ val qty_full_name = dest_Type_name qty
+ val qty_name = Binding.name (Long_Name.base_name qty_full_name)
val qualify = Binding.qualify_name true qty_name
val notes1 = case opt_reflp_thm of
SOME reflp_thm =>
@@ -649,8 +649,8 @@
| _ =>
[typedef_thm, T_def] MRSL @{thm typedef_to_Quotient}
val (rty, qty) = quot_thm_rty_qty quot_thm
- val qty_full_name = (fst o dest_Type) qty
- val qty_name = (Binding.name o Long_Name.base_name) qty_full_name
+ val qty_full_name = dest_Type_name qty
+ val qty_name = Binding.name (Long_Name.base_name qty_full_name)
val qualify = Binding.qualify_name true qty_name
val opt_reflp_thm =
case typedef_set of
@@ -881,7 +881,7 @@
let
val _ = lifting_restore_sanity_check (Context.proof_of ctxt) qinfo
val (_, qty) = quot_thm_rty_qty (#quot_thm qinfo)
- val qty_full_name = (fst o dest_Type) qty
+ val qty_full_name = dest_Type_name qty
val stored_qinfo = Lifting_Info.lookup_quotients (Context.proof_of ctxt) qty_full_name
in
if is_some (stored_qinfo) andalso not (Lifting_Info.quotient_eq (qinfo, (the stored_qinfo)))
--- a/src/HOL/Tools/Lifting/lifting_term.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/Tools/Lifting/lifting_term.ML Sun Aug 04 13:24:54 2024 +0200
@@ -488,7 +488,7 @@
in
if same_type_constrs (rty', qty) then
let
- val distr_rules = get_rel_distr_rules ctxt0 ((fst o dest_Type) rty') (head_of tm)
+ val distr_rules = get_rel_distr_rules ctxt0 (dest_Type_name rty') (head_of tm)
val distr_rule = get_first (prove_extra_assms ctxt0 ctm) distr_rules
in
case distr_rule of
@@ -499,7 +499,7 @@
end
else
let
- val pcrel_def = get_pcrel_def quotients ctxt0 ((fst o dest_Type) qty)
+ val pcrel_def = get_pcrel_def quotients ctxt0 (dest_Type_name qty)
val pcrel_const = (head_of o fst o Logic.dest_equals o Thm.prop_of) pcrel_def
in
if same_constants pcrel_const (head_of trans_rel) then
@@ -548,7 +548,7 @@
else
if is_Type qty then
let
- val q = (fst o dest_Type) qty
+ val q = dest_Type_name qty
in
let
val (rty', rtyq) = gen_instantiate_rtys quotients ctxt (rty, qty)
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Sun Aug 04 13:24:54 2024 +0200
@@ -800,7 +800,7 @@
| \<^Const_>\<open>Trueprop for \<^Const_>\<open>part_equivp _ for _\<close>\<close> => true
| _ => raise NOT_SUPPORTED "Ill-formed quotient type equivalence \
\relation theorem"
- val Ts' = qtyp |> dest_Type |> snd
+ val Ts' = dest_Type_args qtyp
in (subst_atomic_types (Ts' ~~ Ts) equiv_rel, partial) end
| equiv_relation_for_quot_type _ T =
raise TYPE ("Nitpick_HOL.equiv_relation_for_quot_type", [T], [])
@@ -853,7 +853,7 @@
fun is_constr ctxt (x as (_, T)) =
is_nonfree_constr ctxt x andalso
- not (is_interpreted_type (fst (dest_Type (unarize_type (body_type T))))) andalso
+ not (is_interpreted_type (dest_Type_name (unarize_type (body_type T)))) andalso
not (is_stale_constr ctxt x)
val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix
@@ -1643,7 +1643,7 @@
s_betapply [] (fun_t, t)
else if j = n - 1 andalso special_j = ~1 then
optimized_record_update hol_ctxt s
- (rec_T |> dest_Type |> snd |> List.last) fun_t t
+ (List.last (dest_Type_args rec_T)) fun_t t
else
t
end) (index_seq 0 n) Ts
@@ -1965,7 +1965,7 @@
val thy = Proof_Context.theory_of ctxt
val abs_T = domain_type T
in
- typedef_info ctxt (fst (dest_Type abs_T)) |> the
+ typedef_info ctxt (dest_Type_name abs_T) |> the
|> pairf #Abs_inverse #Rep_inverse
|> apply2 (specialize_type thy x o Thm.prop_of o the)
||> single |> op ::
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Sun Aug 04 13:24:54 2024 +0200
@@ -235,7 +235,7 @@
val t1 = do_term new_Ts old_Ts Neut t1
val T1 = fastype_of1 (new_Ts, t1)
val (s1, Ts1) = dest_Type T1
- val T' = hd (snd (dest_Type (hd Ts1)))
+ val T' = hd (dest_Type_args (hd Ts1))
val t2 = Abs (s, T', do_term (T' :: new_Ts) (T :: old_Ts) Neut t2')
val T2 = fastype_of1 (new_Ts, t2)
val t2 = coerce_term hol_ctxt new_Ts (hd Ts1) T2 t2
--- a/src/HOL/Tools/Nunchaku/nunchaku_collect.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku_collect.ML Sun Aug 04 13:24:54 2024 +0200
@@ -249,7 +249,7 @@
(fp,
(case Ts of
[_] => [fp_sugar]
- | _ => map (the o BNF_FP_Def_Sugar.fp_sugar_of ctxt o fst o dest_Type) Ts)
+ | _ => map (the o BNF_FP_Def_Sugar.fp_sugar_of ctxt o dest_Type_name) Ts)
|> map (#ctr_sugar o #fp_ctr_sugar))
| NONE =>
(case Ctr_Sugar.ctr_sugar_of ctxt T_name of
--- a/src/HOL/Tools/Old_Datatype/old_primrec.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_primrec.ML Sun Aug 04 13:24:54 2024 +0200
@@ -60,7 +60,7 @@
else strip_comb (hd middle);
val (cname, T) = dest_Const constr
handle TERM _ => primrec_error "ill-formed constructor";
- val (tname, _) = dest_Type (body_type T) handle TYPE _ =>
+ val tname = dest_Type_name (body_type T) handle TYPE _ =>
primrec_error "cannot determine datatype associated with function"
val (ls, cargs, rs) =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Sun Aug 04 13:24:54 2024 +0200
@@ -479,7 +479,7 @@
let
val tab = Ctr_Sugar.ctr_sugars_of ctxt
|> maps (map_filter (try dest_Const) o #ctrs)
- |> map (fn (c, T) => ((c, (fst o dest_Type o body_type) T), BNF_Util.num_binder_types T))
+ |> map (fn (c, T) => ((c, dest_Type_name (body_type T)), BNF_Util.num_binder_types T))
in fn (c, T) =>
case body_type T of
Type (Tname, _) => AList.lookup (op =) tab (c, Tname)
@@ -890,7 +890,7 @@
fun datatype_name_of_case_name thy =
Ctr_Sugar.ctr_sugar_of_case (Proof_Context.init_global thy)
- #> the #> #ctrs #> hd #> fastype_of #> body_type #> dest_Type #> fst
+ #> the #> #ctrs #> hd #> fastype_of #> body_type #> dest_Type_name
fun make_case_comb thy Tcon =
let
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Sun Aug 04 13:24:54 2024 +0200
@@ -130,7 +130,7 @@
fun get_case_rewrite t =
if is_constructor ctxt t then
let
- val SOME {case_thms, ...} = Ctr_Sugar.ctr_sugar_of ctxt (fst (dest_Type (fastype_of t)))
+ val SOME {case_thms, ...} = Ctr_Sugar.ctr_sugar_of ctxt (dest_Type_name (fastype_of t))
in
fold (union Thm.eq_thm) (case_thms :: map get_case_rewrite (snd (strip_comb t))) []
end
@@ -303,7 +303,7 @@
if is_constructor ctxt t then
let
val SOME {case_thms, split_asm, ...} =
- Ctr_Sugar.ctr_sugar_of ctxt (fst (dest_Type (fastype_of t)))
+ Ctr_Sugar.ctr_sugar_of ctxt (dest_Type_name (fastype_of t))
val num_of_constrs = length case_thms
val (_, ts) = strip_comb t
in
--- a/src/HOL/Tools/Quickcheck/abstract_generators.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/Tools/Quickcheck/abstract_generators.ML Sun Aug 04 13:24:54 2024 +0200
@@ -33,7 +33,7 @@
val opt_pred = Option.map (prep_term ctxt) opt_pred_raw
val constrs = map (prep_term ctxt) constrs_raw
val _ = check_constrs ctxt tyco constrs
- val vs = map dest_TFree (snd (dest_Type (body_type (fastype_of (hd constrs)))))
+ val vs = map dest_TFree (dest_Type_args (body_type (fastype_of (hd constrs))))
val name = Long_Name.base_name tyco
fun mk_dconstrs (Const (s, T)) =
(s, map (Old_Datatype_Aux.dtyp_of_typ [(tyco, vs)]) (binder_types T))
@@ -61,7 +61,7 @@
val quickcheck_generator_cmd =
gen_quickcheck_generator
- ((#1 o dest_Type) oo Proof_Context.read_type_name {proper = true, strict = true})
+ (dest_Type_name oo Proof_Context.read_type_name {proper = true, strict = true})
Syntax.read_term
val _ =
--- a/src/HOL/Tools/Quotient/quotient_type.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/Tools/Quotient/quotient_type.ML Sun Aug 04 13:24:54 2024 +0200
@@ -104,7 +104,7 @@
| _ => error "unsupported equivalence theorem"
)
val def_term = Abs ("x", rty, Abs ("y", qty, Abs_body));
- val qty_name = (Binding.name o Long_Name.base_name o fst o dest_Type) qty
+ val qty_name = Binding.name (Long_Name.base_name (dest_Type_name qty))
val cr_rel_name = Binding.prefix_name "cr_" qty_name
val (fixed_def_term, lthy') = yield_singleton (Variable.importT_terms) def_term lthy
val ((_, (_ , def_thm)), lthy'') =
@@ -118,7 +118,7 @@
val (_ $ _ $ abs_fun $ _) = (HOLogic.dest_Trueprop o Thm.prop_of) quot3_thm
val (T_def, lthy') = define_cr_rel equiv_thm abs_fun lthy
val (rty, qty) = (dest_funT o fastype_of) abs_fun
- val qty_name = (Binding.name o Long_Name.base_name o fst o dest_Type) qty
+ val qty_name = Binding.name (Long_Name.base_name (dest_Type_name qty))
val quotient_thm_name = Binding.prefix_name "Quotient_" qty_name
val (reflp_thm, quot_thm) =
(case (HOLogic.dest_Trueprop o Thm.prop_of) equiv_thm of
@@ -140,7 +140,7 @@
let
val (_ $ rel $ abs $ rep) = (HOLogic.dest_Trueprop o Thm.prop_of) quot_thm
val (qtyp, rtyp) = (dest_funT o fastype_of) rep
- val qty_full_name = (fst o dest_Type) qtyp
+ val qty_full_name = dest_Type_name qtyp
fun quotients phi =
Quotient_Info.transform_quotients phi
{qtyp = qtyp, rtyp = rtyp, equiv_rel = rel, equiv_thm = equiv_thm,
--- a/src/HOL/Tools/SMT/smt_datatypes.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/Tools/SMT/smt_datatypes.ML Sun Aug 04 13:24:54 2024 +0200
@@ -52,7 +52,7 @@
: Typedef.info) T Ts =
if can (curry (op RS) @{thm UNIV_I}) Abs_inverse then
let
- val env = snd (Term.dest_Type abs_type) ~~ Ts
+ val env = Term.dest_Type_args abs_type ~~ Ts
val instT = Term.map_atyps (perhaps (AList.lookup (op =) env))
val constr = Const (Abs_name, instT (rep_type --> abs_type))
@@ -77,7 +77,7 @@
SOME {fp, fp_res = {Ts = fp_Ts, ...}, fp_ctr_sugar = {ctr_sugar, ...}, ...} =>
if member (op =) fps fp then
let
- val ns = map (fst o dest_Type) fp_Ts
+ val ns = map dest_Type_name fp_Ts
val mutual_fp_sugars = map_filter (BNF_FP_Def_Sugar.fp_sugar_of ctxt) ns
val Xs = map #X mutual_fp_sugars
val ctrXs_Tsss = map (#ctrXs_Tss o #fp_ctr_sugar) mutual_fp_sugars
--- a/src/HOL/Tools/Transfer/transfer_bnf.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML Sun Aug 04 13:24:54 2024 +0200
@@ -36,7 +36,7 @@
Const (\<^const_name>\<open>Domainp\<close>, PT --> argT --> HOLogic.boolT) $ P
end
-fun type_name_of_bnf bnf = T_of_bnf bnf |> dest_Type |> fst
+fun type_name_of_bnf bnf = dest_Type_name (T_of_bnf bnf)
fun bnf_only_type_ctr f bnf = if is_Type (T_of_bnf bnf) then f bnf else I
--- a/src/HOL/Tools/datatype_simprocs.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/Tools/datatype_simprocs.ML Sun Aug 04 13:24:54 2024 +0200
@@ -59,7 +59,7 @@
sugar
|> #fp_res
|> #Ts
- |> map (dest_Type #> fst)
+ |> map dest_Type_name
fun get_ctors_mutuals ctxt sugar =
let
@@ -79,7 +79,7 @@
(* simproc will not be used for these types *)
val forbidden_types =
([@{typ "bool"}, @{typ "nat"}, @{typ "'a \<times> 'b"}, @{typ "'a + 'b"}]
- |> map (dest_Type #> fst))
+ |> map dest_Type_name)
@ ["List.list", "Option.option"]
(* FIXME: possible improvements:
@@ -92,7 +92,7 @@
val (lhs, rhs) = apply2 Thm.term_of (clhs, crhs)
val cT = Thm.ctyp_of_cterm clhs
val T = Thm.typ_of cT
- val (T_name, T_args) = T |> dest_Type
+ val (T_name, T_args) = dest_Type T
val _ = if member op= forbidden_types T_name then raise NOT_APPLICABLE else ()
val _ = if lhs aconv rhs then raise NOT_APPLICABLE else ()
--- a/src/HOL/Tools/functor.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/Tools/functor.ML Sun Aug 04 13:24:54 2024 +0200
@@ -209,10 +209,10 @@
val (Ts, T1, T2) = split_mapper_typ tyco T
handle List.Empty => bad_typ ();
val _ =
- apply2 ((fn tyco' => if tyco' = tyco then () else bad_typ ()) o fst o dest_Type) (T1, T2)
+ apply2 ((fn tyco' => if tyco' = tyco then () else bad_typ ()) o dest_Type_name) (T1, T2)
handle TYPE _ => bad_typ ();
val (vs1, vs2) =
- apply2 (map dest_TFree o snd o dest_Type) (T1, T2)
+ apply2 (map dest_TFree o dest_Type_args) (T1, T2)
handle TYPE _ => bad_typ ();
val _ = if has_duplicates (eq_fst (op =)) (vs1 @ vs2)
then bad_typ () else ();
--- a/src/Tools/subtyping.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/Tools/subtyping.ML Sun Aug 04 13:24:54 2024 +0200
@@ -949,7 +949,7 @@
val coercions = map (fst o the o Symreltab.lookup tab) path';
val trans_co = singleton (Variable.polymorphic ctxt)
(fold safe_app coercions (mk_identity dummyT));
- val (Ts, Us) = apply2 (snd o Term.dest_Type) (Term.dest_funT (type_of trans_co));
+ val (Ts, Us) = apply2 dest_Type_args (Term.dest_funT (type_of trans_co));
in
(trans_co, ((Ts, Us), coercions))
end;
@@ -967,10 +967,10 @@
val (T1, T2) = Term.dest_funT (fastype_of t)
handle TYPE _ => err_coercion ();
- val (a, Ts) = Term.dest_Type T1
+ val (a, Ts) = dest_Type T1
handle TYPE _ => err_coercion ();
- val (b, Us) = Term.dest_Type T2
+ val (b, Us) = dest_Type T2
handle TYPE _ => err_coercion ();
fun coercion_data_update (tab, G, _) =