# HG changeset patch
# User wenzelm
# Date 1631196034 -7200
# Node ID 0f3ca0cd8071f66b96dac8150ac63c489bb09ce2
# Parent  64be5f22446286b13b9cbd87108663f7b0a22077
clarified signature;

diff -r 64be5f224462 -r 0f3ca0cd8071 src/Pure/cterm_items.ML
--- a/src/Pure/cterm_items.ML	Thu Sep 09 15:55:12 2021 +0200
+++ b/src/Pure/cterm_items.ML	Thu Sep 09 16:00:34 2021 +0200
@@ -20,21 +20,6 @@
 end;
 
 
-structure Thmtab:
-sig
-  include TABLE
-  val thm_cache: (thm -> 'a) -> thm -> 'a
-end =
-struct
-
-structure Table = Table(type key = thm val ord = Thm.thm_ord);
-open Table;
-
-fun thm_cache f = Cache.create empty lookup update f;
-
-end;
-
-
 structure Cterms:
 sig
   include TERM_ITEMS
@@ -54,3 +39,18 @@
 val add_frees = Thm.fold_atomic_cterms {hyps = true} Term.is_Free add_set;
 
 end;
+
+
+structure Thmtab:
+sig
+  include TABLE
+  val thm_cache: (thm -> 'a) -> thm -> 'a
+end =
+struct
+
+structure Table = Table(type key = thm val ord = Thm.thm_ord);
+open Table;
+
+fun thm_cache f = Cache.create empty lookup update f;
+
+end;
diff -r 64be5f224462 -r 0f3ca0cd8071 src/Tools/misc_legacy.ML
--- a/src/Tools/misc_legacy.ML	Thu Sep 09 15:55:12 2021 +0200
+++ b/src/Tools/misc_legacy.ML	Thu Sep 09 16:00:34 2021 +0200
@@ -5,7 +5,6 @@
 
 signature MISC_LEGACY =
 sig
-  val thm_frees: thm -> Cterms.set
   val cterm_frees: cterm -> Cterms.set
   val add_term_names: term * string list -> string list
   val add_term_tvars: term * (indexname * sort) list -> (indexname * sort) list
@@ -26,8 +25,7 @@
 structure Misc_Legacy: MISC_LEGACY =
 struct
 
-val thm_frees = Cterms.build o Thm.fold_atomic_cterms {hyps = true} Term.is_Free Cterms.add_set;
-val cterm_frees = thm_frees o Drule.mk_term;
+val cterm_frees = Cterms.build o Cterms.add_frees o Drule.mk_term;
 
 (*iterate a function over all types in a term*)
 fun it_term_types f =