# HG changeset patch
# User wenzelm
# Date 1425507278 -3600
# Node ID 7ade9a33c65348690d291a7d615f936c6f10a9e9
# Parent  6020e3dec7b5098c4b71082efa2004f59f6a81fb
tuned signature;

diff -r 6020e3dec7b5 -r 7ade9a33c653 src/HOL/Library/Old_SMT/old_smt_utils.ML
--- a/src/HOL/Library/Old_SMT/old_smt_utils.ML	Wed Mar 04 22:56:25 2015 +0100
+++ b/src/HOL/Library/Old_SMT/old_smt_utils.ML	Wed Mar 04 23:14:38 2015 +0100
@@ -39,7 +39,6 @@
   val instT': cterm -> ctyp * cterm -> cterm
 
   (*certified terms*)
-  val certify: Proof.context -> term -> cterm
   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
@@ -160,8 +159,6 @@
 
 (* certified terms *)
 
-fun certify ctxt = Proof_Context.cterm_of ctxt
-
 fun dest_cabs ct ctxt =
   (case Thm.term_of ct of
     Abs _ =>
diff -r 6020e3dec7b5 -r 7ade9a33c653 src/HOL/Library/Old_SMT/old_z3_proof_methods.ML
--- a/src/HOL/Library/Old_SMT/old_z3_proof_methods.ML	Wed Mar 04 22:56:25 2015 +0100
+++ b/src/HOL/Library/Old_SMT/old_z3_proof_methods.ML	Wed Mar 04 23:14:38 2015 +0100
@@ -51,15 +51,15 @@
 fun mk_inv_of ctxt ct =
   let
     val (dT, rT) = Term.dest_funT (Thm.typ_of_cterm ct)
-    val inv = Old_SMT_Utils.certify ctxt (mk_inv_into dT rT)
-    val univ = Old_SMT_Utils.certify ctxt (mk_univ dT)
+    val inv = Proof_Context.cterm_of ctxt (mk_inv_into dT rT)
+    val univ = Proof_Context.cterm_of ctxt (mk_univ dT)
   in Thm.mk_binop inv univ ct end
 
 fun mk_inj_prop ctxt ct =
   let
     val (dT, rT) = Term.dest_funT (Thm.typ_of_cterm ct)
-    val inj = Old_SMT_Utils.certify ctxt (mk_inj_on dT rT)
-    val univ = Old_SMT_Utils.certify ctxt (mk_univ dT)
+    val inj = Proof_Context.cterm_of ctxt (mk_inj_on dT rT)
+    val univ = Proof_Context.cterm_of ctxt (mk_univ dT)
   in Old_SMT_Utils.mk_cprop (Thm.mk_binop inj ct univ) end
 
 
diff -r 6020e3dec7b5 -r 7ade9a33c653 src/HOL/Library/Old_SMT/old_z3_proof_parser.ML
--- a/src/HOL/Library/Old_SMT/old_z3_proof_parser.ML	Wed Mar 04 22:56:25 2015 +0100
+++ b/src/HOL/Library/Old_SMT/old_z3_proof_parser.ML	Wed Mar 04 23:14:38 2015 +0100
@@ -109,7 +109,7 @@
     val max = fold (Integer.max o fst) vars 0
     val ns = fst (Variable.variant_fixes (replicate (max + 1) var_prefix) ctxt)
     fun mk (i, v) =
-      (v, Old_SMT_Utils.certify ctxt (Free (nth ns i, Thm.typ_of_cterm v)))
+      (v, Proof_Context.cterm_of ctxt (Free (nth ns i, Thm.typ_of_cterm v)))
   in map mk vars end
 
 fun close ctxt (ct, vars) =
@@ -120,7 +120,7 @@
 
 
 fun mk_bound ctxt (i, T) =
-  let val ct = Old_SMT_Utils.certify ctxt (Var ((Name.uu, 0), T))
+  let val ct = Proof_Context.cterm_of ctxt (Var ((Name.uu, 0), T))
   in (ct, [(i, ct)]) end
 
 local
@@ -129,7 +129,7 @@
       val cv =
         (case AList.lookup (op =) vars 0 of
           SOME cv => cv
-        | _ => Old_SMT_Utils.certify ctxt (Var ((Name.uu, Thm.maxidx_of_cterm ct + 1), T)))
+        | _ => Proof_Context.cterm_of ctxt (Var ((Name.uu, Thm.maxidx_of_cterm ct + 1), T)))
       fun dec (i, v) = if i = 0 then NONE else SOME (i-1, v)
       val vars' = map_filter dec vars
     in (Thm.apply (Old_SMT_Utils.instT' cv q) (Thm.lambda cv ct), vars') end
@@ -191,7 +191,7 @@
       |> Symtab.fold (Variable.declare_term o snd) terms
 
     fun cert @{const True} = not_false
-      | cert t = Old_SMT_Utils.certify ctxt' t
+      | cert t = Proof_Context.cterm_of ctxt' t
 
   in (typs, Symtab.map (K cert) terms, Inttab.empty, [], [], ctxt') end
 
@@ -207,7 +207,7 @@
   | NONE => cx |> fresh_name (decl_prefix ^ n)
       |> (fn (m, (typs, terms, exprs, steps, vars, ctxt)) =>
            let
-             val upd = Symtab.update (n, Old_SMT_Utils.certify ctxt (Free (m, T)))
+             val upd = Symtab.update (n, Proof_Context.cterm_of ctxt (Free (m, T)))
            in (typs, upd terms, exprs, steps, vars, ctxt) end))
 
 fun mk_typ (typs, _, _, _, _, ctxt) (s as Old_Z3_Interface.Sym (n, _)) = 
diff -r 6020e3dec7b5 -r 7ade9a33c653 src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML
--- a/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML	Wed Mar 04 22:56:25 2015 +0100
+++ b/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML	Wed Mar 04 23:14:38 2015 +0100
@@ -617,7 +617,7 @@
   fun get_vars f mk pred ctxt t =
     Term.fold_aterms f t []
     |> map_filter (fn v =>
-         if pred v then SOME (Old_SMT_Utils.certify ctxt (mk v)) else NONE)
+         if pred v then SOME (Proof_Context.cterm_of ctxt (mk v)) else NONE)
 
   fun close vars f ct ctxt =
     let
diff -r 6020e3dec7b5 -r 7ade9a33c653 src/HOL/Library/Old_SMT/old_z3_proof_tools.ML
--- a/src/HOL/Library/Old_SMT/old_z3_proof_tools.ML	Wed Mar 04 22:56:25 2015 +0100
+++ b/src/HOL/Library/Old_SMT/old_z3_proof_tools.ML	Wed Mar 04 23:14:38 2015 +0100
@@ -156,7 +156,7 @@
     | NONE =>
         let
           val (n, ctxt') = yield_singleton Variable.variant_fixes "x" ctxt
-          val cv = Old_SMT_Utils.certify ctxt'
+          val cv = Proof_Context.cterm_of ctxt'
             (Free (n, map Thm.typ_of_cterm cvs' ---> Thm.typ_of_cterm ct))
           val cu = Drule.list_comb (cv, cvs')
           val e = (t, (cv, fold_rev Thm.lambda cvs' ct))