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 @@ -1446,10 +1446,10 @@
     1.4      fun var s = ATerm (`I s, [])
     1.5      (* Reconstruction in Metis is strangely dependent on these names. *)
     1.6      fun tag tm = ATerm (type_tag, [var "T", tm])
     1.7 -    val tagged_a = tag (var "A")
     1.8 +    val tagged_var = tag (var "A")
     1.9    in
    1.10      Formula (type_tag_idempotence_helper_name, Axiom,
    1.11 -             eq_formula type_enc [] false (tag tagged_a) tagged_a,
    1.12 +             eq_formula type_enc [] false (tag tagged_var) tagged_var,
    1.13               isabelle_info simpN, NONE)
    1.14    end
    1.15  
    1.16 @@ -1602,10 +1602,10 @@
    1.17    | should_guard_var_in_formula pos phi _ name =
    1.18      formula_fold pos (is_var_positively_naked_in_term name) phi false
    1.19  
    1.20 -fun should_generate_tag_equation _ _ _ (SOME true) _ = false
    1.21 -  | should_generate_tag_equation ctxt mono (Tags (_, level, Nonuniform)) _ T =
    1.22 +fun should_generate_tag_bound_decl _ _ _ (SOME true) _ = false
    1.23 +  | should_generate_tag_bound_decl ctxt mono (Tags (_, level, Nonuniform)) _ T =
    1.24      should_encode_type ctxt mono level T
    1.25 -  | should_generate_tag_equation _ _ _ _ _ = false
    1.26 +  | should_generate_tag_bound_decl _ _ _ _ _ = false
    1.27  
    1.28  fun mk_aterm format type_enc name T_args args =
    1.29    ATerm (name, map_filter (ho_term_for_type_arg format type_enc) T_args @ args)
    1.30 @@ -1663,8 +1663,12 @@
    1.31          IVar (name, T)
    1.32          |> type_guard_iterm ctxt format type_enc T
    1.33          |> do_term pos |> AAtom |> SOME
    1.34 -      else if should_generate_tag_equation ctxt mono type_enc universal T then
    1.35 -        NONE (*###*)
    1.36 +      else if should_generate_tag_bound_decl ctxt mono type_enc universal T then
    1.37 +        let
    1.38 +          val var = ATerm (name, [])
    1.39 +          val tagged_var =
    1.40 +            ATerm (type_tag, [ho_term_from_typ format type_enc T, var])
    1.41 +        in SOME (AAtom (ATerm (`I tptp_equal, [tagged_var, var]))) end
    1.42        else
    1.43          NONE
    1.44      fun do_formula pos (AQuant (q, xs, phi)) =
    1.45 @@ -1955,7 +1959,7 @@
    1.46               isabelle_info introN, NONE)
    1.47    end
    1.48  
    1.49 -fun formula_lines_for_lightweight_tags_sym_decl ctxt format conj_sym_kind mono
    1.50 +fun formula_lines_for_nonuniform_tags_sym_decl ctxt format conj_sym_kind mono
    1.51          type_enc n s (j, (s', T_args, T, pred_sym, ary, in_conj)) =
    1.52    let
    1.53      val ident_base =
    1.54 @@ -2033,7 +2037,7 @@
    1.55       | Nonuniform =>
    1.56         let val n = length decls in
    1.57           (0 upto n - 1 ~~ decls)
    1.58 -         |> maps (formula_lines_for_lightweight_tags_sym_decl ctxt format
    1.59 +         |> maps (formula_lines_for_nonuniform_tags_sym_decl ctxt format
    1.60                        conj_sym_kind mono type_enc n s)
    1.61         end)
    1.62