mangle tag bound declarations properly
authorblanchet
Fri Aug 26 00:19:25 2011 +0200 (2011-08-26)
changeset 445052c1fc7b29c9c
parent 44504 6f29df8d2007
child 44506 7e3913e70846
mangle tag bound declarations properly
src/HOL/Tools/ATP/atp_translate.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Fri Aug 26 00:05:45 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Fri Aug 26 00:19:25 2011 +0200
     1.3 @@ -1671,8 +1671,7 @@
     1.4        else if should_generate_tag_bound_decl ctxt mono type_enc universal T then
     1.5          let
     1.6            val var = ATerm (name, [])
     1.7 -          val tagged_var =
     1.8 -            ATerm (type_tag, [ho_term_from_typ format type_enc T, var])
     1.9 +          val tagged_var = var |> tag_with_type ctxt format mono type_enc pos T
    1.10          in SOME (AAtom (ATerm (`I tptp_equal, [tagged_var, var]))) end
    1.11        else
    1.12          NONE