tune bound names

--- a/src/HOL/Tools/Sledgehammer/meson_clausify.ML	Fri Oct 01 16:13:28 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/meson_clausify.ML	Fri Oct 01 16:58:56 2010 +0200
@@ -304,7 +304,7 @@
     if new_skolemizer then
       let
         fun skolemize choice_ths =
-          Meson.skolemize ctxt choice_ths
+          Meson.skolemize_with_choice_thms ctxt choice_ths
           #> simplify (ss_only @{thms all_simps[symmetric]})
         val pull_out =
           simplify (ss_only @{thms all_simps[symmetric] ex_simps[symmetric]})

--- a/src/HOL/Tools/meson.ML	Fri Oct 01 16:13:28 2010 +0200
+++ b/src/HOL/Tools/meson.ML	Fri Oct 01 16:58:56 2010 +0200
@@ -15,7 +15,8 @@
   val finish_cnf: thm list -> thm list
   val presimplify: thm -> thm
   val make_nnf: Proof.context -> thm -> thm
-  val skolemize : Proof.context -> thm list -> thm -> thm
+  val skolemize_with_choice_thms : Proof.context -> thm list -> thm -> thm
+  val skolemize : Proof.context -> thm -> thm
   val is_fol_term: theory -> term -> bool
   val make_clauses_unsorted: thm list -> thm list
   val make_clauses: thm list -> thm list
@@ -105,10 +106,24 @@
     SOME th => th
   | NONE => raise THM ("first_order_resolve", 0, [thA, thB]))
 
-(*Forward proof while preserving bound variables names*)
+(* Applying "choice" swaps the bound variable names. We tweak
+   "Thm.rename_boundvars"'s input to get the desired names. *)
+fun tweak_bounds (_ $ (Const (@{const_name Ex}, _)
+                       $ Abs (_, _, Const (@{const_name All}, _) $ _)))
+                 (t0 $ (Const (@{const_name All}, T1)
+                        $ Abs (a1, T1', Const (@{const_name Ex}, T2)
+                                        $ Abs (a2, T2', t')))) =
+    t0 $ (Const (@{const_name All}, T1)
+          $ Abs (a2, T1', Const (@{const_name Ex}, T2) $ Abs (a1, T2', t')))
+  | tweak_bounds _ t = t
+
+(* Forward proof while preserving bound variables names*)
 fun rename_bvs_RS th rl =
-  let val th' = th RS rl
-  in  Thm.rename_boundvars (concl_of th') (concl_of th) th' end;
+  let
+    val th' = th RS rl
+    val t = concl_of th
+    val t' = concl_of th'
+  in Thm.rename_boundvars t' (tweak_bounds t' t) th' end
 
 (*raises exception if no rules apply*)
 fun tryres (th, rls) =
@@ -530,7 +545,7 @@
 
 (* Pull existential quantifiers to front. This accomplishes Skolemization for
    clauses that arise from a subgoal. *)
-fun skolemize ctxt choice_ths =
+fun skolemize_with_choice_thms ctxt choice_ths =
   let
     fun aux th =
       if not (has_conns [@{const_name Ex}] (prop_of th)) then
@@ -548,9 +563,11 @@
                       |> forward_res ctxt aux
   in aux o make_nnf ctxt end
 
+fun skolemize ctxt = skolemize_with_choice_thms ctxt (Meson_Choices.get ctxt)
+
 (* "RS" can fail if "unify_search_bound" is too small. *)
 fun try_skolemize ctxt th =
-  try (skolemize ctxt (Meson_Choices.get ctxt)) th
+  try (skolemize ctxt) th
   |> tap (fn NONE => trace_msg (fn () => "Failed to skolemize " ^
                                          Display.string_of_thm ctxt th)
            | _ => ())