# HG changeset patch
# User blanchet
# Date 1409179238 -7200
# Node ID e9ab6f4c650be867f78e3e24b3ee3781174fd3d1
# Parent  663ae2463f32bc23db53e19619fabe707b7efa97
keep skolems as is -- otherwise this breaks proof steps that refer to variables that were 'obtain'ed in the outer Isar proof

diff -r 663ae2463f32 -r e9ab6f4c650b src/HOL/Tools/SMT/smtlib_isar.ML
--- a/src/HOL/Tools/SMT/smtlib_isar.ML	Thu Aug 28 00:40:38 2014 +0200
+++ b/src/HOL/Tools/SMT/smtlib_isar.ML	Thu Aug 28 00:40:38 2014 +0200
@@ -8,11 +8,11 @@
 signature SMTLIB_ISAR =
 sig
   val unlift_term: term list -> term -> term
-  val postprocess_step_conclusion: theory -> thm list -> term list -> term -> term
+  val postprocess_step_conclusion: Proof.context -> thm list -> term list -> term -> term
   val normalizing_prems : Proof.context -> term -> (string * string list) list
   val distinguish_conjecture_and_hypothesis : ''a list -> ''b -> ''b -> ''b list ->
     (''a * 'c) list -> 'c list -> 'c -> (ATP_Problem.atp_formula_role * 'c) option
-  val unskolemize_names: term -> term
+  val unskolemize_names: Proof.context -> term -> term
 end;
 
 structure SMTLIB_Isar: SMTLIB_ISAR =
@@ -34,18 +34,22 @@
     and un_term t = map_aterms un_free t
   in un_term end
 
-(* It is not entirely clear why this should be necessary, especially for abstractions variables. *)
-val unskolemize_names =
+(* Remove the "__" suffix for newly introduced variables (Skolems). It is not clear why "__" is
+   generated also for abstraction variables, but this is repaired here. *)
+fun unskolemize_names ctxt =
   Term.map_abs_vars (perhaps (try Name.dest_skolem))
-  #> Term.map_aterms (perhaps (try (fn Free (s, T) => Free (Name.dest_skolem s, T))))
+  #> Term.map_aterms (perhaps (try (fn Free (s, T) =>
+    Free (s |> not (Variable.is_fixed ctxt s) ? Name.dest_skolem, T))))
 
-fun postprocess_step_conclusion thy rewrite_rules ll_defs =
-  Raw_Simplifier.rewrite_term thy rewrite_rules []
-  #> Object_Logic.atomize_term thy
-  #> not (null ll_defs) ? unlift_term ll_defs
-  #> simplify_bool
-  #> unskolemize_names
-  #> HOLogic.mk_Trueprop
+fun postprocess_step_conclusion ctxt rewrite_rules ll_defs =
+  let val thy = Proof_Context.theory_of ctxt in
+    Raw_Simplifier.rewrite_term thy rewrite_rules []
+    #> Object_Logic.atomize_term thy
+    #> not (null ll_defs) ? unlift_term ll_defs
+    #> simplify_bool
+    #> unskolemize_names ctxt
+    #> HOLogic.mk_Trueprop
+  end
 
 fun normalizing_prems ctxt concl0 =
   SMT_Normalize.case_bool_entry :: SMT_Normalize.special_quant_table @
diff -r 663ae2463f32 -r e9ab6f4c650b src/HOL/Tools/SMT/verit_isar.ML
--- a/src/HOL/Tools/SMT/verit_isar.ML	Thu Aug 28 00:40:38 2014 +0200
+++ b/src/HOL/Tools/SMT/verit_isar.ML	Thu Aug 28 00:40:38 2014 +0200
@@ -26,11 +26,10 @@
 fun atp_proof_of_veriT_proof ctxt ll_defs rewrite_rules hyp_ts concl_t fact_helper_ts prem_ids
     conjecture_id fact_helper_ids proof =
   let
-    val thy = Proof_Context.theory_of ctxt
     fun steps_of (VeriT_Proof.VeriT_Step {id, rule, prems, concl, ...}) =
       let
-        val concl' = postprocess_step_conclusion thy rewrite_rules ll_defs concl
-        fun standard_step role = ((id, []), role, concl', rule, map (fn id => (id, [])) prems)
+        val concl' = postprocess_step_conclusion ctxt rewrite_rules ll_defs concl
+        fun standard_step role = ((id, []), role, concl', rule, map (rpair []) prems)
       in
         if rule = veriT_input_rule then
           let val ss = the_list (AList.lookup (op =) fact_helper_ids (the (Int.fromString id))) in
@@ -40,7 +39,7 @@
             | SOME (role0, concl00) =>
               let
                 val name0 = (id ^ "a", ss)
-                val concl0 = unskolemize_names concl00
+                val concl0 = unskolemize_names ctxt concl00
               in
                 [(name0, role0, concl0, rule, []),
                  ((id, []), Plain, concl', veriT_rewrite_rule,
diff -r 663ae2463f32 -r e9ab6f4c650b src/HOL/Tools/SMT/z3_isar.ML
--- a/src/HOL/Tools/SMT/z3_isar.ML	Thu Aug 28 00:40:38 2014 +0200
+++ b/src/HOL/Tools/SMT/z3_isar.ML	Thu Aug 28 00:40:38 2014 +0200
@@ -77,15 +77,13 @@
 fun atp_proof_of_z3_proof ctxt ll_defs rewrite_rules hyp_ts concl_t fact_helper_ts prem_ids
     conjecture_id fact_helper_ids proof =
   let
-    val thy = Proof_Context.theory_of ctxt
-
     fun steps_of (Z3_Proof.Z3_Step {id, rule, prems, concl, ...}) =
       let
         val sid = string_of_int id
 
         val concl' = concl
           |> reorder_foralls (* crucial for skolemization steps *)
-          |> postprocess_step_conclusion thy rewrite_rules ll_defs
+          |> postprocess_step_conclusion ctxt rewrite_rules ll_defs
         fun standard_step role =
           ((sid, []), role, concl', Z3_Proof.string_of_rule rule,
            map (fn id => (string_of_int id, [])) prems)
@@ -99,7 +97,7 @@
             | SOME (role0, concl00) =>
               let
                 val name0 = (sid ^ "a", ss)
-                val concl0 = unskolemize_names concl00
+                val concl0 = unskolemize_names ctxt concl00
               in
                 (if role0 = Axiom then []
                  else [(name0, role0, concl0, Z3_Proof.string_of_rule rule, [])]) @