1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Mon Jun 06 20:36:35 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Mon Jun 06 20:36:35 2011 +0200
     1.3 @@ -1299,10 +1299,10 @@
     1.4    let
     1.5      fun var s = ATerm (`I s, [])
     1.6      fun tag tm = ATerm (type_tag, [var "T", tm])
     1.7 -    val tagged_x = tag (var "X")
     1.8 +    val tagged_a = tag (var "A")
     1.9    in
    1.10      Formula (type_tag_idempotence_helper_name, Axiom,
    1.11 -             AAtom (ATerm (`I tptp_equal, [tag tagged_x, tagged_x]))
    1.12 +             AAtom (ATerm (`I tptp_equal, [tag tagged_a, tagged_a]))
    1.13               |> close_formula_universally, simp_info, NONE)
    1.14    end
    1.15