# HG changeset patch
# User blanchet
# Date 1411979979 -7200
# Node ID 6ade4c7109a8502beca440480abe1a845a557ad7
# Parent  4508b6bff67154207f57d78a5bc71dce1e658cbd
make sure no '__' suffixes make it until Isar proof

diff -r 4508b6bff671 -r 6ade4c7109a8 src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Mon Sep 29 10:39:39 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Mon Sep 29 10:39:39 2014 +0200
@@ -240,10 +240,14 @@
         in
           (Prove (qs, xs', l, t', subs', facts, meths, comment), subst_ctxt')
         end
-    and rationalize_proof outer subst_ctxt (Proof (fix, assms, steps)) =
+    and rationalize_proof outer (subst_ctxt as (subst, ctxt)) (Proof (fix, assms, steps)) =
       let
         val (fix', subst_ctxt' as (subst', _)) =
-          if outer then (fix, subst_ctxt) else rename_obtains fix subst_ctxt
+          if outer then
+            (* last call: eliminate any remaining skolem names (from SMT proofs) *)
+            (fix, (subst @ map (fn x => (Free (apfst Name.skolem x), Free x)) fix, ctxt))
+          else
+            rename_obtains fix subst_ctxt
       in
         Proof (fix', map (apsnd (subst_atomic subst')) assms,
           fst (fold_map rationalize_step steps subst_ctxt'))