# HG changeset patch
# User wenzelm
# Date 1630921184 -7200
# Node ID 5e3f4efa87f9a98f262396b7c1f45a26c9fa6bda
# Parent  eb265f54e3ce32356dd1e555bba3364448e8e0b9
unused;

diff -r eb265f54e3ce -r 5e3f4efa87f9 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Mon Sep 06 11:32:18 2021 +0200
+++ b/src/Pure/more_thm.ML	Mon Sep 06 11:39:44 2021 +0200
@@ -26,7 +26,6 @@
   val eq_ctyp: ctyp * ctyp -> bool
   val aconvc: cterm * cterm -> bool
   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
@@ -142,8 +141,6 @@
   Thm.fold_atomic_ctyps {hyps = false} (fn a => is_TVar (Thm.typ_of a) ? insert eq_ctyp a);
 val add_vars =
   Thm.fold_atomic_cterms {hyps = false} (fn a => is_Var (Thm.term_of a) ? insert (op aconvc) a);
-val add_frees =
-  Thm.fold_atomic_cterms {hyps = true} (fn a => is_Free (Thm.term_of a) ? insert (op aconvc) a);
 
 fun frees_of th =
   (th, (Term_Subst.Frees.empty, [])) |-> Thm.fold_atomic_cterms {hyps = true}