# HG changeset patch
# User blanchet
# Date 1406897037 -7200
# Node ID c65c116553b5aaa3d4fb012634dcb8a31f4500ce
# Parent  a68b8db8691d005b753f1f6e0cf6b5a78421df68
more rational unskolemizing of names

diff -r a68b8db8691d -r c65c116553b5 src/HOL/Tools/SMT2/smtlib2_isar.ML
--- a/src/HOL/Tools/SMT2/smtlib2_isar.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/SMT2/smtlib2_isar.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -65,7 +65,6 @@
   |> not (null ll_defs) ? unlift_term ll_defs
   |> unskolemize_names
   |> HOLogic.mk_Trueprop
-  |> unskolemize_names
 
 fun normalizing_prems ctxt concl0 =
   SMT2_Normalize.case_bool_entry :: SMT2_Normalize.special_quant_table @
diff -r a68b8db8691d -r c65c116553b5 src/HOL/Tools/SMT2/verit_isar.ML
--- a/src/HOL/Tools/SMT2/verit_isar.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/SMT2/verit_isar.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -42,7 +42,7 @@
                 val name0 = (id ^ "a", ss)
                 val concl0 = unskolemize_names concl00
               in
-                [(name0, role0, unskolemize_names concl0, rule, []),
+                [(name0, role0, concl0, rule, []),
                  ((id, []), Plain, concl', veriT_rewrite_rule,
                   name0 :: normalizing_prems ctxt concl0)]
               end)
diff -r a68b8db8691d -r c65c116553b5 src/HOL/Tools/SMT2/z3_new_isar.ML
--- a/src/HOL/Tools/SMT2/z3_new_isar.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_isar.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -83,8 +83,11 @@
             (case distinguish_conjecture_and_hypothesis ss id conjecture_id prem_ids fact_helper_ts
                 hyp_ts concl_t concl of
               NONE => []
-            | SOME (role0, concl0) =>
-              let val name0 = (sid ^ "a", ss) in
+            | SOME (role0, concl00) =>
+              let
+                val name0 = (sid ^ "a", ss)
+                val concl0 = unskolemize_names concl00
+              in
                 (if role0 = Axiom then []
                  else [(name0, role0, concl0, Z3_New_Proof.string_of_rule rule, [])]) @
                 [((sid, []), Plain, concl', Z3_New_Proof.string_of_rule Z3_New_Proof.Rewrite,