# HG changeset patch
# User blanchet
# Date 1406897037 -7200
# Node ID 816f96fff418c9758b7473839f3ce52e176801cc
# Parent  5a57e10ebb0f0f000eb24b4d95b96649ad121280
tuned name context code

diff -r 5a57e10ebb0f -r 816f96fff418 src/HOL/Tools/SMT2/smtlib2_proof.ML
--- a/src/HOL/Tools/SMT2/smtlib2_proof.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/SMT2/smtlib2_proof.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -21,8 +21,7 @@
     ('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
+    term * ((string * (string * typ)) list, 'b) context) -> ('c, 'b) context -> (term * string list)
 
   (*type and term parsers*)
   type type_parser = SMTLIB2.tree * typ list -> typ option
@@ -56,7 +55,7 @@
   extra: 'a}
 
 fun mk_context ctxt id syms typs funs extra: ('a, 'b) context =
-  {ctxt=ctxt, id=id, syms=syms, typs=typs, funs=funs, extra=extra}
+  {ctxt = ctxt, id = id, syms = syms, typs = typs, funs = funs, extra = extra}
 
 fun empty_context ctxt typs funs = mk_context ctxt 1 Symtab.empty typs funs []
 
@@ -93,11 +92,11 @@
       singleton (Proof_Context.standard_term_check_finish ctxt)
     fun infer ctxt t = if needs_infer t then infer_types ctxt t else t
 
-    val (t, {ctxt=ctxt', extra=names, ...}: ((string * (string * typ)) list, '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
-    ((t', map fst names), mk_context ctxt id syms typs funs extra)
+    (t', map fst names)
   end
 
 fun lookup_typ ({typs, ...}: ('a, 'b) context) = Symtab.lookup typs
diff -r 5a57e10ebb0f -r 816f96fff418 src/HOL/Tools/SMT2/verit_proof.ML
--- a/src/HOL/Tools/SMT2/verit_proof.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/SMT2/verit_proof.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -62,7 +62,7 @@
 
 fun node_of p cx =
   ([], cx)
-  ||>> with_fresh_names (term_of p)
+  ||>> `(with_fresh_names (term_of p))
   |>> snd
 
 (*in order to get Z3-style quantification*)
diff -r 5a57e10ebb0f -r 816f96fff418 src/HOL/Tools/SMT2/z3_new_proof.ML
--- a/src/HOL/Tools/SMT2/z3_new_proof.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_proof.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -159,7 +159,7 @@
       in
         cx
         |> fold_map node_of ps
-        ||>> with_fresh_names (term_of p)
+        ||>> `(with_fresh_names (term_of p))
         ||>> next_id
         |>> (fn ((prems, (t, ns)), id) => mk_node id r prems t ns)
       end