--- a/src/HOL/Tools/SMT/smt_util.ML Wed Mar 04 20:50:20 2015 +0100
+++ b/src/HOL/Tools/SMT/smt_util.ML Wed Mar 04 22:05:01 2015 +0100
@@ -45,7 +45,6 @@
val instT': cterm -> ctyp * cterm -> cterm
(*certified terms*)
- val typ_of: cterm -> typ
val dest_cabs: cterm -> Proof.context -> cterm * Proof.context
val dest_all_cabs: cterm -> Proof.context -> cterm * Proof.context
val dest_cbinder: cterm -> Proof.context -> cterm * Proof.context
@@ -167,20 +166,18 @@
fun mk_const_pat thy name destT =
let val cpat = Thm.cterm_of thy (Const (name, Sign.the_const_type thy name))
- in (destT (Thm.ctyp_of_term cpat), cpat) end
+ in (destT (Thm.ctyp_of_cterm cpat), cpat) end
val destT1 = hd o Thm.dest_ctyp
val destT2 = hd o tl o Thm.dest_ctyp
fun instTs cUs (cTs, ct) = Thm.instantiate_cterm (cTs ~~ cUs, []) ct
fun instT cU (cT, ct) = instTs [cU] ([cT], ct)
-fun instT' ct = instT (Thm.ctyp_of_term ct)
+fun instT' ct = instT (Thm.ctyp_of_cterm ct)
(* certified terms *)
-fun typ_of ct = #T (Thm.rep_cterm ct)
-
fun dest_cabs ct ctxt =
(case Thm.term_of ct of
Abs _ =>