--- a/src/Pure/more_thm.ML Sun Sep 05 19:47:06 2021 +0200
+++ b/src/Pure/more_thm.ML Sun Sep 05 21:09:31 2021 +0200
@@ -28,6 +28,7 @@
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 frees_of: thm -> cterm list
val dest_funT: ctyp -> ctyp * ctyp
val strip_type: ctyp -> ctyp list * ctyp
val all_name: Proof.context -> string * cterm -> cterm -> cterm
@@ -141,6 +142,17 @@
val add_frees = Thm.fold_atomic_cterms (fn a => is_Free (Thm.term_of a) ? insert (op aconvc) a);
val add_vars = Thm.fold_atomic_cterms (fn a => is_Var (Thm.term_of a) ? insert (op aconvc) a);
+fun frees_of th =
+ (th, (Term_Subst.Frees.empty, [])) |-> Thm.fold_atomic_cterms
+ (fn a => fn (set, list) =>
+ (case Thm.term_of a of
+ Free v =>
+ if not (Term_Subst.Frees.defined set v)
+ then (Term_Subst.Frees.add (v, ()) set, a :: list)
+ else (set, list)
+ | _ => (set, list)))
+ |> #2;
+
(* ctyp operations *)