# HG changeset patch # User wenzelm # Date 1630864026 -7200 # Node ID a810e8f2f2e92157a0de994da01a0d9e0cba00a8 # Parent 4426b52eabb4e70bf1bb55a4abe9e1de36d2b5dc unused; diff -r 4426b52eabb4 -r a810e8f2f2e9 src/Pure/drule.ML --- 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;