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