# HG changeset patch
# User wenzelm
# Date 1433024435 -7200
# Node ID 9b3b812e695727d68a9ae9edc7de3ce85b797d31
# Parent  05fabeb0130a04a18eb81c80de33fb9bc05cb408
obsolete;

diff -r 05fabeb0130a -r 9b3b812e6957 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Sun May 31 00:17:47 2015 +0200
+++ b/src/Pure/drule.ML	Sun May 31 00:20:35 2015 +0200
@@ -13,7 +13,6 @@
   val strip_imp_prems: cterm -> cterm list
   val strip_imp_concl: cterm -> cterm
   val cprems_of: thm -> cterm list
-  val cterm_fun: (term -> term) -> (cterm -> cterm)
   val forall_intr_list: cterm list -> thm -> thm
   val forall_intr_vars: thm -> thm
   val forall_elim_list: cterm list -> thm -> thm
@@ -130,8 +129,6 @@
 (*The premises of a theorem, as a cterm list*)
 val cprems_of = strip_imp_prems o Thm.cprop_of;
 
-fun cterm_fun f ct = Thm.global_cterm_of (Thm.theory_of_cterm ct) (f (Thm.term_of ct));
-
 fun certify t = Thm.global_cterm_of (Context.the_theory (Context.the_thread_data ())) t;
 
 val implies = certify Logic.implies;