--- a/src/HOL/Tools/SMT2/smtlib2_proof.ML Wed Jun 11 19:32:12 2014 +0200
+++ b/src/HOL/Tools/SMT2/smtlib2_proof.ML Wed Jun 11 19:32:39 2014 +0200
@@ -19,6 +19,10 @@
val update_binding: string * 'b shared -> ('a, 'b) context -> ('a, 'b) context
val with_bindings: (string * 'b shared) list -> (('a, 'b) context -> 'c * ('d, 'b) context) ->
('a, 'b) context -> 'c * ('d, 'b) context
+ val next_id: ('a, 'b) context -> int * ('a, 'b) context
+ val with_fresh_names: (('a list, 'b) context ->
+ term * ((string * (string * typ)) list, 'b) context) -> ('c, 'b) context ->
+ (term * string list) * ('c, 'b) context
(*type and term parsers*)
type type_parser = SMTLIB2.tree * typ list -> typ option
@@ -89,8 +93,7 @@
singleton (Proof_Context.standard_term_check_finish ctxt)
fun infer ctxt t = if needs_infer t then infer_types ctxt t else t
- type bindings = (string * (string * typ)) list
- val (t, {ctxt=ctxt', extra=names, ...}: (bindings, 'b) context) =
+ val (t, {ctxt=ctxt', extra=names, ...}: ((string * (string * typ)) list, 'b) context) =
f (mk_context ctxt id syms typs funs [])
val t' = infer ctxt' (fold_rev bind names (HOLogic.mk_Trueprop t))
in
--- a/src/HOL/Tools/SMT2/z3_new_real.ML Wed Jun 11 19:32:12 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_real.ML Wed Jun 11 19:32:39 2014 +0200
@@ -25,8 +25,8 @@
| _ => pair NONE)
val _ = Theory.setup (Context.theory_map (
- SMT2LIB_Proof.add_type_parser real_type_parser #>
- SMT2LIB_Proof.add_term_parser real_term_parser #>
+ SMTLIB2_Proof.add_type_parser real_type_parser #>
+ SMTLIB2_Proof.add_term_parser real_term_parser #>
Z3_New_Replay_Methods.add_arith_abstracter abstract))
end