# HG changeset patch
# User wenzelm
# Date 1182724600 -7200
# Node ID c13ca04303ded097a75f911394186dee148ce7e3
# Parent  1dfbfc92017ab0591cd6ef05e51b5538e58f98fb
added reasonably efficient add_cterm_frees;

diff -r 1dfbfc92017a -r c13ca04303de src/Pure/more_thm.ML
--- 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;