# HG changeset patch
# User blanchet
# Date 1407229673 -7200
# Node ID d1cf76cef93bb0f8e546757a8fc4f50e68fc382e
# Parent  9cb24c8352842e745b0f00dc5e8b13f0cc1794c7
tuned skolemization

diff -r 9cb24c835284 -r d1cf76cef93b src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Tue Aug 05 10:59:40 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Tue Aug 05 11:07:53 2014 +0200
@@ -218,12 +218,14 @@
     relabel_proof [] 0
   end
 
+fun stutter_single_letter s = String.extract (s, 0, SOME 1) ^ s
+
 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_names0 = map (stutter_single_letter 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