# HG changeset patch
# User wenzelm
# Date 1737483999 -3600
# Node ID ee680c69de38a2074220ffa394c312950a544bcb
# Parent  23957ebffaf766548779237b1866ef0cbf0d66c7
misc tuning: prefer specific variants of Thm.dest_comb;

diff -r 23957ebffaf7 -r ee680c69de38 src/HOL/HOLCF/Cfun.thy
--- 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>;
diff -r 23957ebffaf7 -r ee680c69de38 src/HOL/Import/import_rule.ML
--- 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
diff -r 23957ebffaf7 -r ee680c69de38 src/HOL/Library/Code_Abstract_Nat.thy
--- 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))]
       | _ $ _ =>
diff -r 23957ebffaf7 -r ee680c69de38 src/HOL/Nominal/nominal_inductive.ML
--- 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;
diff -r 23957ebffaf7 -r ee680c69de38 src/HOL/Nominal/nominal_inductive2.ML
--- 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;
diff -r 23957ebffaf7 -r ee680c69de38 src/HOL/Real_Asymp/exp_log_expression.ML
--- 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
diff -r 23957ebffaf7 -r ee680c69de38 src/HOL/Statespace/state_space.ML
--- 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);
diff -r 23957ebffaf7 -r ee680c69de38 src/HOL/Tools/Function/partial_function.ML
--- 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 ***)
diff -r 23957ebffaf7 -r ee680c69de38 src/HOL/Tools/Meson/meson_clausify.ML
--- 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 =
diff -r 23957ebffaf7 -r ee680c69de38 src/HOL/Tools/datatype_simprocs.ML
--- 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