# HG changeset patch
# User wenzelm
# Date 1439663243 -7200
# Node ID dc5b7982e324bb9c2f51e2d3cd740900834c6592
# Parent  b316f218ef348928bf9dec0618f5761d014ae19a
obsolete;

diff -r b316f218ef34 -r dc5b7982e324 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sat Aug 15 20:07:05 2015 +0200
+++ b/src/Pure/thm.ML	Sat Aug 15 20:27:23 2015 +0200
@@ -21,13 +21,11 @@
 sig
   include BASIC_THM
   (*certified types*)
-  val theory_of_ctyp: ctyp -> theory
   val typ_of: ctyp -> typ
   val global_ctyp_of: theory -> typ -> ctyp
   val ctyp_of: Proof.context -> typ -> ctyp
   val dest_ctyp: ctyp -> ctyp list
   (*certified terms*)
-  val theory_of_cterm: cterm -> theory
   val term_of: cterm -> term
   val typ_of_cterm: cterm -> typ
   val ctyp_of_cterm: cterm -> ctyp
@@ -159,7 +157,6 @@
 abstype ctyp = Ctyp of {thy: theory, T: typ, maxidx: int, sorts: sort Ord_List.T}
 with
 
-fun theory_of_ctyp (Ctyp {thy, ...}) = thy;
 fun typ_of (Ctyp {T, ...}) = T;
 
 fun global_ctyp_of thy raw_T =
@@ -185,7 +182,6 @@
 
 exception CTERM of string * cterm list;
 
-fun theory_of_cterm (Cterm {thy, ...}) = thy;
 fun term_of (Cterm {t, ...}) = t;
 
 fun typ_of_cterm (Cterm {T, ...}) = T;