# HG changeset patch
# User wenzelm
# Date 1433014081 -7200
# Node ID 6e465f0d46d3270f25c717941561992c1fbde287
# Parent  2a0b42cd58fba60d7cd9d0f93d343cb52fed46d8
obsolete;

diff -r 2a0b42cd58fb -r 6e465f0d46d3 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Sat May 30 20:21:53 2015 +0200
+++ b/src/Pure/drule.ML	Sat May 30 21:28:01 2015 +0200
@@ -14,7 +14,6 @@
   val strip_imp_concl: cterm -> cterm
   val cprems_of: thm -> cterm list
   val cterm_fun: (term -> term) -> (cterm -> cterm)
-  val ctyp_fun: (typ -> typ) -> (ctyp -> ctyp)
   val forall_intr_list: cterm list -> thm -> thm
   val forall_intr_vars: thm -> thm
   val forall_elim_list: cterm list -> thm -> thm
@@ -133,7 +132,6 @@
 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 ctyp_fun f cT = Thm.global_ctyp_of (Thm.theory_of_ctyp cT) (f (Thm.typ_of cT));
 
 fun certify t = Thm.global_cterm_of (Context.the_theory (Context.the_thread_data ())) t;