--- a/src/HOL/HOLCF/Cfun.thy Tue Jan 21 19:26:09 2025 +0100
+++ b/src/HOL/HOLCF/Cfun.thy Tue Jan 21 19:26:39 2025 +0100
@@ -144,7 +144,7 @@
simproc_setup beta_cfun_proc ("Rep_cfun (Abs_cfun f)") = \<open>
K (fn ctxt => fn ct =>
let
- val f = #2 (Thm.dest_comb (#2 (Thm.dest_comb ct)));
+ val f = Thm.dest_arg (Thm.dest_arg ct);
val [T, U] = Thm.dest_ctyp (Thm.ctyp_of_cterm f);
val tr = Thm.instantiate' [SOME T, SOME U] [SOME f] (mk_meta_eq @{thm Abs_cfun_inverse2});
val rules = Named_Theorems.get ctxt \<^named_theorems>\<open>cont2cont\<close>;
--- a/src/HOL/Import/import_rule.ML Tue Jan 21 19:26:09 2025 +0100
+++ b/src/HOL/Import/import_rule.ML Tue Jan 21 19:26:39 2025 +0100
@@ -281,8 +281,7 @@
(SOME typedef_bindings) (fn ctxt => resolve_tac ctxt [th2] 1)) thy
val aty = Thm.global_ctyp_of thy' (#abs_type (#1 typedef_info))
val th = freezeT thy' (#type_definition (#2 typedef_info))
- val (rep, abs) =
- Thm.dest_comb (#1 (Thm.dest_comb (HOLogic.dest_judgment (Thm.cprop_of th)))) |>> Thm.dest_arg
+ val (rep, abs) = Thm.dest_binop (Thm.dest_fun (HOLogic.dest_judgment (Thm.cprop_of th)))
val [A, B] = Thm.dest_ctyp (Thm.ctyp_of_cterm rep)
val typedef_th = typedef_hol2hollight A B rep abs cP (Thm.free ("a", aty)) (Thm.free ("r", ctT))
in
--- a/src/HOL/Library/Code_Abstract_Nat.thy Tue Jan 21 19:26:09 2025 +0100
+++ b/src/HOL/Library/Code_Abstract_Nat.thy Tue Jan 21 19:26:39 2025 +0100
@@ -59,8 +59,8 @@
val vname = singleton (Name.variant_list (map fst
(fold (Term.add_var_names o Thm.full_prop_of) thms []))) "n";
val cv = Thm.cterm_of ctxt (Var ((vname, 0), HOLogic.natT));
- val lhs_of = snd o Thm.dest_comb o fst o Thm.dest_comb o Thm.cprop_of;
- val rhs_of = snd o Thm.dest_comb o Thm.cprop_of;
+ val lhs_of = Thm.dest_arg1 o Thm.cprop_of;
+ val rhs_of = Thm.dest_arg o Thm.cprop_of;
fun find_vars ct = (case Thm.term_of ct of
(Const (\<^const_name>\<open>Suc\<close>, _) $ Var _) => [(cv, snd (Thm.dest_comb ct))]
| _ $ _ =>
--- a/src/HOL/Nominal/nominal_inductive.ML Tue Jan 21 19:26:09 2025 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML Tue Jan 21 19:26:39 2025 +0100
@@ -33,8 +33,8 @@
val perm_bool = mk_meta_eq @{thm perm_bool_def};
val perm_boolI = @{thm perm_boolI};
-val (_, [perm_boolI_pi, _]) = Drule.strip_comb (snd (Thm.dest_comb
- (Drule.strip_imp_concl (Thm.cprop_of perm_boolI))));
+val (_, [perm_boolI_pi, _]) = Drule.strip_comb (Thm.dest_arg
+ (Drule.strip_imp_concl (Thm.cprop_of perm_boolI)));
fun mk_perm_bool ctxt pi th =
th RS infer_instantiate ctxt [(#1 (dest_Var (Thm.term_of perm_boolI_pi)), pi)] perm_boolI;
--- a/src/HOL/Nominal/nominal_inductive2.ML Tue Jan 21 19:26:09 2025 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML Tue Jan 21 19:26:39 2025 +0100
@@ -37,8 +37,8 @@
val perm_bool = mk_meta_eq @{thm perm_bool_def};
val perm_boolI = @{thm perm_boolI};
-val (_, [perm_boolI_pi, _]) = Drule.strip_comb (snd (Thm.dest_comb
- (Drule.strip_imp_concl (Thm.cprop_of perm_boolI))));
+val (_, [perm_boolI_pi, _]) = Drule.strip_comb (Thm.dest_arg
+ (Drule.strip_imp_concl (Thm.cprop_of perm_boolI)));
fun mk_perm_bool ctxt pi th =
th RS infer_instantiate ctxt [(#1 (dest_Var (Thm.term_of perm_boolI_pi)), pi)] perm_boolI;
--- a/src/HOL/Real_Asymp/exp_log_expression.ML Tue Jan 21 19:26:09 2025 +0100
+++ b/src/HOL/Real_Asymp/exp_log_expression.ML Tue Jan 21 19:26:39 2025 +0100
@@ -192,9 +192,9 @@
fun rewrite ctxt thms ct =
let
val thm1 = Thm.eta_long_conversion ct
- val rhs = thm1 |> Thm.cprop_of |> Thm.dest_comb |> snd
+ val rhs = thm1 |> Thm.cprop_of |> Thm.dest_arg
val (thm2, prems) = rewrite' ctxt [] [] thms rhs
- val rhs = thm2 |> Thm.cprop_of |> Thm.dest_comb |> snd
+ val rhs = thm2 |> Thm.cprop_of |> Thm.dest_arg
val thm3 = Thm.eta_conversion rhs
val thm = Thm.transitive thm1 (Thm.transitive thm2 thm3)
in
--- a/src/HOL/Statespace/state_space.ML Tue Jan 21 19:26:09 2025 +0100
+++ b/src/HOL/Statespace/state_space.ML Tue Jan 21 19:26:39 2025 +0100
@@ -239,7 +239,7 @@
fun get_paths dist_thm =
let
- val ctree = Thm.cprop_of dist_thm |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
+ val ctree = Thm.cprop_of dist_thm |> Thm.dest_arg |> Thm.dest_arg;
val tree = Thm.term_of ctree;
val x_path = the (DistinctTreeProver.find_tree x tree);
val y_path = the (DistinctTreeProver.find_tree y tree);
--- a/src/HOL/Tools/Function/partial_function.ML Tue Jan 21 19:26:09 2025 +0100
+++ b/src/HOL/Tools/Function/partial_function.ML Tue Jan 21 19:26:39 2025 +0100
@@ -129,7 +129,7 @@
end;
fun head_conv cv ct =
- if can Thm.dest_comb ct then Conv.fun_conv (head_conv cv) ct else cv ct;
+ if can Thm.dest_fun ct then Conv.fun_conv (head_conv cv) ct else cv ct;
(*** currying transformation ***)
--- a/src/HOL/Tools/Meson/meson_clausify.ML Tue Jan 21 19:26:09 2025 +0100
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Tue Jan 21 19:26:39 2025 +0100
@@ -197,7 +197,7 @@
fun old_skolem_theorem_of_def ctxt rhs0 =
let
val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> Thm.cterm_of ctxt
- val rhs' = rhs |> Thm.dest_comb |> snd
+ val rhs' = rhs |> Thm.dest_arg
val (ch, frees) = c_variant_abs_multi (rhs', [])
val (hilbert, cabs) = ch |> Thm.dest_comb |>> Thm.term_of
val T =
--- a/src/HOL/Tools/datatype_simprocs.ML Tue Jan 21 19:26:09 2025 +0100
+++ b/src/HOL/Tools/datatype_simprocs.ML Tue Jan 21 19:26:39 2025 +0100
@@ -88,7 +88,7 @@
*)
fun no_proper_subterm_proc ctxt ct =
let
- val (clhs, crhs) = ct |> Thm.dest_comb |> apfst (Thm.dest_comb #> snd)
+ val (clhs, crhs) = Thm.dest_binop ct
val (lhs, rhs) = apply2 Thm.term_of (clhs, crhs)
val cT = Thm.ctyp_of_cterm clhs
val T = Thm.typ_of cT