# HG changeset patch
# User wenzelm
# Date 1723368740 -7200
# Node ID 434cf7a5bf932a1e5d8441e943b96784e0b6d6cd
# Parent  b21af525f543ea9d8bb3220aae1f49e74ef95d78
tuned modules;

diff -r b21af525f543 -r 434cf7a5bf93 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Sat Aug 10 21:32:10 2024 +0200
+++ b/src/Pure/more_thm.ML	Sun Aug 11 11:32:20 2024 +0200
@@ -23,6 +23,8 @@
   val aconvc: cterm * cterm -> bool
   val add_tvars: thm -> ctyp TVars.table -> ctyp TVars.table
   val add_vars: thm -> cterm Vars.table -> cterm Vars.table
+  val dest_ctyp0: ctyp -> ctyp
+  val dest_ctyp1: ctyp -> ctyp
   val dest_funT: ctyp -> ctyp * ctyp
   val strip_type: ctyp -> ctyp list * ctyp
   val instantiate_ctyp: ctyp TVars.table -> ctyp -> ctyp
@@ -143,6 +145,9 @@
 
 (* ctyp operations *)
 
+val dest_ctyp0 = Thm.dest_ctypN 0;
+val dest_ctyp1 = Thm.dest_ctypN 1;
+
 fun dest_funT cT =
   (case Thm.typ_of cT of
     Type ("fun", _) => let val [A, B] = Thm.dest_ctyp cT in (A, B) end
diff -r b21af525f543 -r 434cf7a5bf93 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sat Aug 10 21:32:10 2024 +0200
+++ b/src/Pure/thm.ML	Sun Aug 11 11:32:20 2024 +0200
@@ -30,8 +30,6 @@
   val ctyp_of: Proof.context -> typ -> ctyp
   val dest_ctyp: ctyp -> ctyp list
   val dest_ctypN: int -> ctyp -> ctyp
-  val dest_ctyp0: ctyp -> ctyp
-  val dest_ctyp1: ctyp -> ctyp
   val make_ctyp: ctyp -> ctyp list -> ctyp
   (*certified terms*)
   val term_of: cterm -> term
@@ -226,9 +224,6 @@
     | _ => err ())
   end;
 
-val dest_ctyp0 = dest_ctypN 0;
-val dest_ctyp1 = dest_ctypN 1;
-
 fun join_certificate_ctyp (Ctyp {cert, ...}) cert0 = Context.join_certificate (cert0, cert);
 fun union_sorts_ctyp (Ctyp {sorts, ...}) sorts0 = Sorts.union sorts0 sorts;
 fun maxidx_ctyp (Ctyp {maxidx, ...}) maxidx0 = Int.max (maxidx0, maxidx);