--- 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;
--- 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 =