# 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