# HG changeset patch
# User blanchet
# Date 1407229180 -7200
# Node ID 9cb24c8352842e745b0f00dc5e8b13f0cc1794c7
# Parent  d80d3fb5627042e7d70ae36dfdcee362f96e1aa4
rationalize Skolem names

diff -r d80d3fb56270 -r 9cb24c835284 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Tue Aug 05 10:17:15 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Tue Aug 05 10:59:40 2014 +0200
@@ -31,6 +31,7 @@
   val forall_of : term -> term -> term
   val exists_of : term -> term -> term
   val simplify_bool : term -> term
+  val var_name_of_typ : typ -> string
   val rename_bound_vars : term -> term
   val type_enc_aliases : (string * string list) list
   val unalias_type_enc : string -> string list
diff -r d80d3fb56270 -r 9cb24c835284 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Aug 05 10:17:15 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Aug 05 10:59:40 2014 +0200
@@ -361,7 +361,8 @@
           ||> (comment_isar_proof comment_of
                #> chain_isar_proof
                #> kill_useless_labels_in_isar_proof
-               #> relabel_isar_proof_nicely)
+               #> relabel_isar_proof_nicely
+               #> rationalize_obtains_in_isar_proofs ctxt)
       in
         (case add_isar_steps (steps_of_isar_proof isar_proof) 0 of
           1 =>
diff -r d80d3fb56270 -r 9cb24c835284 src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Tue Aug 05 10:17:15 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Tue Aug 05 10:59:40 2014 +0200
@@ -46,6 +46,7 @@
   val kill_useless_labels_in_isar_proof : isar_proof -> isar_proof
   val relabel_isar_proof_canonically : isar_proof -> isar_proof
   val relabel_isar_proof_nicely : isar_proof -> isar_proof
+  val rationalize_obtains_in_isar_proofs : Proof.context -> isar_proof -> isar_proof
 
   val string_of_isar_proof : Proof.context -> int -> int -> isar_proof -> string
 end;
@@ -217,6 +218,33 @@
     relabel_proof [] 0
   end
 
+fun rationalize_obtains_in_isar_proofs ctxt =
+  let
+    fun rename_obtains xs (subst, ctxt) =
+      let
+        val Ts = map snd xs
+        val new_names0 = map (prefix "some_" o var_name_of_typ o body_type) Ts
+        val (new_names, ctxt') = Variable.variant_fixes new_names0 ctxt
+        val ys = map2 pair new_names Ts
+      in
+        (ys, ((map Free xs ~~ map Free ys) @ subst, ctxt'))
+      end
+
+    fun rationalize_step (Prove (qs, xs, l, t, subs, facts, meths, comment)) subst_ctxt =
+        let
+          val (xs', subst_ctxt' as (subst', _)) = rename_obtains xs subst_ctxt
+          val t' = subst_atomic subst' t
+          val subs' = map (rationalize_proof subst_ctxt') subs
+        in
+          (Prove (qs, xs', l, t', subs', facts, meths, comment), subst_ctxt')
+        end
+    and rationalize_proof (subst_ctxt as (subst, _)) (Proof (fix, assms, steps)) =
+      Proof (fix, map (apsnd (subst_atomic subst)) assms,
+        fst (fold_map rationalize_step steps subst_ctxt))
+  in
+    rationalize_proof ([], ctxt)
+  end
+
 val indent_size = 2
 
 fun string_of_isar_proof ctxt0 i n proof =