--- a/src/Pure/drule.ML Sun Sep 05 19:47:06 2021 +0200
+++ b/src/Pure/drule.ML Sun Sep 05 21:09:31 2021 +0200
@@ -89,7 +89,7 @@
val mk_term: cterm -> thm
val dest_term: thm -> cterm
val cterm_rule: (thm -> thm) -> cterm -> cterm
- val cterm_add_frees: cterm -> cterm list -> cterm list
+ val cterm_frees_of: cterm -> cterm list
val dummy_thm: thm
val free_dummy_thm: thm
val is_sort_constraint: term -> bool
@@ -615,7 +615,7 @@
end;
fun cterm_rule f = dest_term o f o mk_term;
-val cterm_add_frees = Thm.add_frees o mk_term;
+val cterm_frees_of = Thm.frees_of o mk_term;
val dummy_thm = mk_term (certify Term.dummy_prop);
val free_dummy_thm = Thm.tag_free_dummy dummy_thm;