# HG changeset patch
# User wenzelm
# Date 1555166539 -7200
# Node ID 6218698851b9c65ff255d75504b461c675c416c2
# Parent  78fffdfc678705daa0556438207a13be8518e34f
tuned signature -- more ctyp operations;

diff -r 78fffdfc6787 -r 6218698851b9 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Sat Apr 13 16:33:33 2019 +0200
+++ b/src/Pure/drule.ML	Sat Apr 13 16:42:19 2019 +0200
@@ -56,7 +56,6 @@
   val generalize: string list * string list -> thm -> thm
   val list_comb: cterm * cterm list -> cterm
   val strip_comb: cterm -> cterm * cterm list
-  val strip_type: ctyp -> ctyp list * ctyp
   val beta_conv: cterm -> cterm -> cterm
   val flexflex_unique: Proof.context option -> thm -> thm
   val export_without_context: thm -> thm
@@ -155,15 +154,6 @@
       in stripc (ct1, ct2 :: cts) end handle CTERM _ => p
   in stripc (ct, []) end;
 
-(* cterm version of strip_type: maps  [T1,...,Tn]--->T  to   ([T1,T2,...,Tn], T) *)
-fun strip_type cT = (case Thm.typ_of cT of
-    Type ("fun", _) =>
-      let
-        val [cT1, cT2] = Thm.dest_ctyp cT;
-        val (cTs, cT') = strip_type cT2
-      in (cT1 :: cTs, cT') end
-  | _ => ([], cT));
-
 (*Beta-conversion for cterms, where x is an abstraction. Simply returns the rhs
   of the meta-equality returned by the beta_conversion rule.*)
 fun beta_conv x y =
diff -r 78fffdfc6787 -r 6218698851b9 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Sat Apr 13 16:33:33 2019 +0200
+++ b/src/Pure/more_thm.ML	Sat Apr 13 16:42:19 2019 +0200
@@ -28,6 +28,8 @@
   val add_tvars: thm -> ctyp list -> ctyp list
   val add_frees: thm -> cterm list -> cterm list
   val add_vars: thm -> cterm list -> cterm list
+  val dest_ctyp_fun: ctyp -> ctyp * ctyp
+  val strip_type: ctyp -> ctyp list * ctyp
   val all_name: Proof.context -> string * cterm -> cterm -> cterm
   val all: Proof.context -> cterm -> cterm -> cterm
   val mk_binop: cterm -> cterm -> cterm -> cterm
@@ -142,6 +144,29 @@
 val add_vars = Thm.fold_atomic_cterms (fn a => is_Var (Thm.term_of a) ? insert (op aconvc) a);
 
 
+(* ctyp destructors *)
+
+fun dest_ctyp_fun cT =
+  let
+    val T = Thm.typ_of cT;
+    fun dest_ctyp_nth i = Thm.dest_ctyp_nth i cT;
+  in
+    (case T of
+      Type ("fun", _) => (dest_ctyp_nth 0, dest_ctyp_nth 1)
+    | _ => raise TYPE ("dest_ctyp_fun", [T], []))
+  end;
+
+(* ctyp version of strip_type: maps  [T1,...,Tn]--->T  to   ([T1,T2,...,Tn], T) *)
+fun strip_type cT =
+  (case Thm.typ_of cT of
+    Type ("fun", _) =>
+      let
+        val (cT1, cT2) = dest_ctyp_fun cT;
+        val (cTs, cT') = strip_type cT2
+      in (cT1 :: cTs, cT') end
+  | _ => ([], cT));
+
+
 (* cterm constructors and destructors *)
 
 fun all_name ctxt (x, t) A =