# HG changeset patch
# User wenzelm
# Date 1139338611 -3600
# Node ID 49aa2c8791baf83c608f69cf66572dc97b15f70c
# Parent  52639ad19a968922acb8696e65bc053782877060
removed obsolete sign_of_cterm;
adapted Sign.certify_term;

diff -r 52639ad19a96 -r 49aa2c8791ba src/Pure/thm.ML
--- a/src/Pure/thm.ML	Tue Feb 07 19:56:50 2006 +0100
+++ b/src/Pure/thm.ML	Tue Feb 07 19:56:51 2006 +0100
@@ -34,7 +34,6 @@
   val crep_cterm: cterm ->
     {thy: theory, sign: theory, t: term, T: ctyp, maxidx: int, sorts: sort list}
   val theory_of_cterm: cterm -> theory
-  val sign_of_cterm: cterm -> theory    (*obsolete*)
   val term_of: cterm -> term
   val cterm_of: theory -> term -> cterm
   val ctyp_of_term: cterm -> ctyp
@@ -229,8 +228,6 @@
   end;
 
 fun theory_of_cterm (Cterm {thy_ref, ...}) = Theory.deref thy_ref;
-val sign_of_cterm = theory_of_cterm;
-
 fun term_of (Cterm {t, ...}) = t;
 
 fun ctyp_of_term (Cterm {thy_ref, T, sorts, ...}) =
@@ -238,7 +235,7 @@
 
 fun cterm_of thy tm =
   let
-    val (t, T, maxidx) = Sign.certify_term (Sign.pp thy) thy tm;
+    val (t, T, maxidx) = Sign.certify_term thy tm;
     val sorts = may_insert_term_sorts thy t [];
   in Cterm {thy_ref = Theory.self_ref thy, t = t, T = T, maxidx = maxidx, sorts = sorts} end;
 
@@ -1515,8 +1512,7 @@
     fn (thy2, data) =>
       let
         val thy' = Theory.merge (Theory.deref thy_ref1, thy2);
-        val (prop, T, maxidx) =
-          Sign.certify_term (Sign.pp thy') thy' (oracle (thy', data));
+        val (prop, T, maxidx) = Sign.certify_term thy' (oracle (thy', data));
       in
         if T <> propT then
           raise THM ("Oracle's result must have type prop: " ^ name, 0, [])