--- 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 =
--- 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 =