# HG changeset patch
# User blanchet
# Date 1307385395 -7200
# Node ID cb8b9786ffe3339d3ef46ab7b0f6feb6bd9a278b
# Parent  831d28439b3a9bd5a000fa8fe5a824dd2d842f56
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"

diff -r 831d28439b3a -r cb8b9786ffe3 src/HOL/Tools/ATP/atp_translate.ML
--- 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