--- a/src/HOL/Tools/SMT/smt_util.ML Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Tools/SMT/smt_util.ML Tue Mar 03 19:08:04 2015 +0100
@@ -45,7 +45,6 @@
val instT': cterm -> ctyp * cterm -> cterm
(*certified terms*)
- val certify: Proof.context -> term -> cterm
val typ_of: cterm -> typ
val dest_cabs: cterm -> Proof.context -> cterm * Proof.context
val dest_all_cabs: cterm -> Proof.context -> cterm * Proof.context
@@ -180,8 +179,6 @@
(* certified terms *)
-fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt)
-
fun typ_of ct = #T (Thm.rep_cterm ct)
fun dest_cabs ct ctxt =