change var name as a workaround for rare issue in Metis's reconstruction code -- namely, "find_var" fails because "X = X" is wrongly mirrorred as "A = A"

--- a/src/HOL/Tools/ATP/atp_translate.ML	Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Mon Jun 06 20:36:35 2011 +0200
@@ -1299,10 +1299,10 @@
   let
     fun var s = ATerm (`I s, [])
     fun tag tm = ATerm (type_tag, [var "T", tm])
-    val tagged_x = tag (var "X")
+    val tagged_a = tag (var "A")
   in
     Formula (type_tag_idempotence_helper_name, Axiom,
-             AAtom (ATerm (`I tptp_equal, [tag tagged_x, tagged_x]))
+             AAtom (ATerm (`I tptp_equal, [tag tagged_a, tagged_a]))
              |> close_formula_universally, simp_info, NONE)
   end