--- a/src/Pure/more_thm.ML Mon Jun 25 00:36:39 2007 +0200
+++ b/src/Pure/more_thm.ML Mon Jun 25 00:36:40 2007 +0200
@@ -10,6 +10,8 @@
signature THM =
sig
include THM
+ val aconvc : cterm * cterm -> bool
+ val add_cterm_frees: cterm -> cterm list -> cterm list
val mk_binop: cterm -> cterm -> cterm -> cterm
val dest_binop: cterm -> cterm * cterm
val dest_implies: cterm -> cterm * cterm
@@ -19,7 +21,6 @@
val lhs_of: thm -> cterm
val rhs_of: thm -> cterm
val thm_ord: thm * thm -> order
- val aconvc : cterm * cterm -> bool
val eq_thm: thm * thm -> bool
val eq_thms: thm list * thm list -> bool
val eq_thm_thy: thm * thm -> bool
@@ -52,6 +53,17 @@
(** basic operations **)
+(* collecting cterms *)
+
+val op aconvc = op aconv o pairself Thm.term_of;
+
+fun add_cterm_frees ct =
+ let
+ val cert = Thm.cterm_of (Thm.theory_of_cterm ct);
+ val t = Thm.term_of ct;
+ in Term.fold_aterms (fn v as Free _ => insert (op aconvc) (cert v) | _ => I) t end;
+
+
(* cterm constructors and destructors *)
fun mk_binop c a b = Thm.capply (Thm.capply c a) b;
@@ -102,8 +114,6 @@
(* equality *)
-val op aconvc = op aconv o pairself Thm.term_of;
-
fun eq_thm ths =
Context.joinable (pairself Thm.theory_of_thm ths) andalso
thm_ord ths = EQUAL;