# HG changeset patch
# User blanchet
# Date 1394713094 -3600
# Node ID 3e717b56e955e88487ac2514a4c1a8f46cea2751
# Parent  f68150e2ead3a567d9f24340b38a37ee43649e5b
avoid names that may clash with Z3's output (e.g. '')

diff -r f68150e2ead3 -r 3e717b56e955 src/HOL/Tools/SMT2/smt2_solver.ML
--- a/src/HOL/Tools/SMT2/smt2_solver.ML	Thu Mar 13 13:18:14 2014 +0100
+++ b/src/HOL/Tools/SMT2/smt2_solver.ML	Thu Mar 13 13:18:14 2014 +0100
@@ -231,13 +231,9 @@
   let
     val (ithms, ctxt) = SMT2_Normalize.normalize iwthms ctxt0
     val (name, {command, replay, ...}) = name_and_info_of ctxt
-  in
-    invoke name command ithms ctxt
-    |> replay ctxt
-  end
+  in replay ctxt (invoke name command ithms ctxt) end
 
 val default_max_relevant = #default_max_relevant oo get_info
-
 val supports_filter = #supports_filter o snd o name_and_info_of 
 
 
diff -r f68150e2ead3 -r 3e717b56e955 src/HOL/Tools/SMT2/smt2_translate.ML
--- a/src/HOL/Tools/SMT2/smt2_translate.ML	Thu Mar 13 13:18:14 2014 +0100
+++ b/src/HOL/Tools/SMT2/smt2_translate.ML	Thu Mar 13 13:18:14 2014 +0100
@@ -91,14 +91,14 @@
   | suggested_name_of_term _ = Name.uu
 
 val empty_tr_context = (Name.context, Typtab.empty, Termtab.empty)
-val safe_prefix = "$"
+val safe_suffix = "$"
 
 fun add_typ T proper (cx as (names, typs, terms)) =
   (case Typtab.lookup typs T of
     SOME (name, _) => (name, cx)
   | NONE =>
       let
-        val sugg = safe_prefix ^ Name.desymbolize true (suggested_name_of_typ T)
+        val sugg = Name.desymbolize true (suggested_name_of_typ T) ^ safe_suffix
         val (name, names') = Name.variant sugg names
         val typs' = Typtab.update (T, (name, proper)) typs
       in (name, (names', typs', terms)) end)
@@ -108,7 +108,7 @@
     SOME (name, _) => (name, cx)
   | NONE => 
       let
-        val sugg = safe_prefix ^ Name.desymbolize false (suggested_name_of_term t)
+        val sugg = Name.desymbolize false (suggested_name_of_term t) ^ safe_suffix
         val (name, names') = Name.variant sugg names
         val terms' = Termtab.update (t, (name, sort)) terms
       in (name, (names', typs, terms')) end)
diff -r f68150e2ead3 -r 3e717b56e955 src/HOL/Tools/SMT2/z3_new_replay.ML
--- a/src/HOL/Tools/SMT2/z3_new_replay.ML	Thu Mar 13 13:18:14 2014 +0100
+++ b/src/HOL/Tools/SMT2/z3_new_replay.ML	Thu Mar 13 13:18:14 2014 +0100
@@ -110,10 +110,7 @@
       let
         val (thm, ctxt') = if exact then (Thm.implies_elim thm1 th, ctxt) else assume thm1 ctxt
         val thms' = if exact then thms else th :: thms
-      in 
-        ((insert (op =) i is, thms'),
-          (ctxt', Inttab.update (id, (fixes, thm)) ptab))
-      end
+      in ((insert (op =) i is, thms'), (ctxt', Inttab.update (id, (fixes, thm)) ptab)) end
 
     fun add (Z3_New_Proof.Z3_Step {id, rule, concl, fixes, ...})
         (cx as ((is, thms), (ctxt, ptab))) =