# HG changeset patch # User wenzelm # Date 1722770694 -7200 # Node ID a90ab1ea6458bf31c45ae1da516376e560616ad4 # Parent 276b07a1b5f5e6adf24bc92999a6251578a8a42a tuned: more explicit dest_Type_name and dest_Type_args; diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/HOLCF/Tools/Domain/domain.ML --- 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) diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/HOLCF/Tools/Domain/domain_axioms.ML --- 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 *) diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/HOLCF/Tools/Domain/domain_constructors.ML --- 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 diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/HOLCF/Tools/Domain/domain_induction.ML --- 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 = diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML --- 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>\cpo\) 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>\cpo\) 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 diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/HOLCF/Tools/cpodef.ML --- 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, diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/HOLCF/ex/Pattern_Match.thy --- 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>\pcpo\); fun pat_lhs (pat, args) = diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/Import/import_data.ML --- 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 diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/Library/case_converter.ML --- 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 diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/Library/code_lazy.ML --- 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 diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/Library/datatype_records.ML --- 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 diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/Library/refute.ML --- 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 _ = diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/Library/simps_case_conv.ML --- 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 diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/List.thy --- 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 diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/Nominal/nominal_datatype.ML --- 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>\finite\, 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 diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/Nominal/nominal_inductive.ML --- 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>\type\ 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"; diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/Nominal/nominal_inductive2.ML --- 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>\type\ 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>\Fun.id\, 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"); diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/Nominal/nominal_primrec.ML --- 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) = diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/Quickcheck_Examples/Quickcheck_Nesting.thy --- 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>\compat\; 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 diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/Statespace/distinct_tree_prover.ML --- 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>\Tip\, 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), diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/Tools/ATP/atp_problem_generate.ML --- 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) = diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/Tools/BNF/bnf_comp.ML --- 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>\id_bnf\, _)) = Const (\<^const_name>\id_bnf\, 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; diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- 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 []) diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML --- 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; diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/Tools/BNF/bnf_gfp_grec.ML --- 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; diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML --- 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; diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- 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); diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/Tools/BNF/bnf_lfp_compat.ML --- 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 diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/Tools/BNF/bnf_lfp_countable.ML --- 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; diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML --- 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; diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/Tools/BNF/bnf_lfp_size.ML --- 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); diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/Tools/BNF/bnf_lift.ML --- 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); diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/Tools/Ctr_Sugar/case_translation.ML --- 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; diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- 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; diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/Tools/Function/function_elims.ML --- 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>\bool\)); val sumtree_inj = Sum_Tree.mk_inj domT n_fs (idx + 1) args; diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/Tools/Lifting/lifting_bnf.ML --- 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)} diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/Tools/Lifting/lifting_def_code_dt.ML --- 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.") diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/Tools/Lifting/lifting_info.ML --- 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) diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/Tools/Lifting/lifting_setup.ML --- 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))) diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/Tools/Lifting/lifting_term.ML --- 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) diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/Tools/Nitpick/nitpick_hol.ML --- 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_>\Trueprop for \<^Const_>\part_equivp _ for _\\ => 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 :: diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/Tools/Nitpick/nitpick_preproc.ML --- 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 diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/Tools/Nunchaku/nunchaku_collect.ML --- 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 diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/Tools/Old_Datatype/old_primrec.ML --- 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) = diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- 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 diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML --- 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 diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/Tools/Quickcheck/abstract_generators.ML --- 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 _ = diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/Tools/Quotient/quotient_type.ML --- 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, diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/Tools/SMT/smt_datatypes.ML --- 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 diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/Tools/Transfer/transfer_bnf.ML --- 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>\Domainp\, 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 diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/Tools/datatype_simprocs.ML --- 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 \ '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 () diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/Tools/functor.ML --- 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 (); diff -r 276b07a1b5f5 -r a90ab1ea6458 src/Tools/subtyping.ML --- 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, _) =