# HG changeset patch
# User blanchet
# Date 1285948592 -7200
# Node ID b0be1daf0667d6582dd696a0c9abd1bf890fadf2
# Parent  864bfafcf2510d6a4f7c1a08e3884d96ee78cada
rename bound variables after skolemizing, if the axiom of choice is available

diff -r 864bfafcf251 -r b0be1daf0667 src/HOL/Tools/Sledgehammer/meson_clausify.ML
--- a/src/HOL/Tools/Sledgehammer/meson_clausify.ML	Fri Oct 01 17:52:20 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/meson_clausify.ML	Fri Oct 01 17:56:32 2010 +0200
@@ -312,8 +312,10 @@
   in
     if new_skolemizer then
       let
-        val t = concl_of th
-        val th = Thm.rename_boundvars t (rename_vars_to_be_zapped ax_no t) th
+        fun rename_bound_vars th =
+          let val t = concl_of th in
+            th |> Thm.rename_boundvars t (rename_vars_to_be_zapped ax_no t)
+          end
         fun skolemize choice_ths =
           Meson.skolemize_with_choice_thms ctxt choice_ths
           #> simplify (ss_only @{thms all_simps[symmetric]})
@@ -321,9 +323,9 @@
           simplify (ss_only @{thms all_simps[symmetric] ex_simps[symmetric]})
         val (discharger_th, fully_skolemized_th) =
           if null choice_ths then
-            (th |> pull_out, th |> skolemize [no_choice])
+            th |> rename_bound_vars |> `I |>> pull_out ||> skolemize [no_choice]
           else
-            th |> skolemize choice_ths |> `I
+            th |> skolemize choice_ths |> rename_bound_vars |> `I
         val t =
           fully_skolemized_th |> cprop_of
           |> zap true |> Drule.export_without_context