src/HOL/Tools/ATP/atp_translate.ML
changeset 44408 30ea62ab4f16
parent 44406 392c69bdb170
child 44410 8801a1eef30a
     1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Mon Aug 22 15:02:45 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Mon Aug 22 15:02:45 2011 +0200
     1.3 @@ -1444,9 +1444,8 @@
     1.4  fun type_tag_idempotence_fact type_enc =
     1.5    let
     1.6      fun var s = ATerm (`I s, [])
     1.7 -    (* Reconstruction in Metis is strangely dependent on these names. *)
     1.8 -    fun tag tm = ATerm (type_tag, [var "T", tm])
     1.9 -    val tagged_var = tag (var "A")
    1.10 +    fun tag tm = ATerm (type_tag, [var "A", tm])
    1.11 +    val tagged_var = tag (var "X")
    1.12    in
    1.13      Formula (type_tag_idempotence_helper_name, Axiom,
    1.14               eq_formula type_enc [] false (tag tagged_var) tagged_var,