src/HOL/Tools/SMT/z3_proof_tools.ML

 end
 
 structure Z3_Proof_Tools: Z3_PROOF_TOOLS =
 struct
 
+structure U = SMT_Utils
 structure I = Z3_Interface
 
 
 
 (* accessing terms *)

 fun term_of ct = dest_prop (Thm.term_of ct)
 fun prop_of thm = dest_prop (Thm.prop_of thm)
 
 val mk_prop = Thm.capply (Thm.cterm_of @{theory} @{const Trueprop})
 
-val eq = I.mk_inst_pair I.destT1 @{cpat "op =="}
-fun mk_meta_eq_cterm ct cu = Thm.mk_binop (I.instT' ct eq) ct cu
-
-fun as_meta_eq ct = uncurry mk_meta_eq_cterm (Thm.dest_binop (Thm.dest_arg ct))
+fun as_meta_eq ct = uncurry U.mk_cequals (Thm.dest_binop (Thm.dest_arg ct))
 
 
 
 (* theorem nets *)
 

 (* |- c x == t x ==> P (c x)  ~~>  c == t |- P (c x) *) 
 fun make_hyp_def thm ctxt =
   let
     val (lhs, rhs) = Thm.dest_binop (Thm.cprem_of thm 1)
     val (cf, cvs) = Drule.strip_comb lhs
-    val eq = mk_meta_eq_cterm cf (fold_rev Thm.cabs cvs rhs)
+    val eq = U.mk_cequals cf (fold_rev Thm.cabs cvs rhs)
     fun apply cv th =
       Thm.combination th (Thm.reflexive cv)
       |> Conv.fconv_rule (Conv.arg_conv (Thm.beta_conversion false))
   in
     yield_singleton Assumption.add_assumes eq ctxt