# 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, [])