--- a/src/Pure/drule.ML Sun Sep 05 19:38:36 2021 +0200
+++ b/src/Pure/drule.ML Sun Sep 05 19:47:06 2021 +0200
@@ -90,7 +90,6 @@
val dest_term: thm -> cterm
val cterm_rule: (thm -> thm) -> cterm -> cterm
val cterm_add_frees: cterm -> cterm list -> cterm list
- val cterm_add_vars: cterm -> cterm list -> cterm list
val dummy_thm: thm
val free_dummy_thm: thm
val is_sort_constraint: term -> bool
@@ -616,9 +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_add_vars = Thm.add_vars o mk_term;
val dummy_thm = mk_term (certify Term.dummy_prop);
val free_dummy_thm = Thm.tag_free_dummy dummy_thm;