# HG changeset patch
# User blanchet
# Date 1314310765 -7200
# Node ID 2c1fc7b29c9c485a3034192956b20e0ff0d0b2b2
# Parent  6f29df8d20077de822f31c14edc23c9c783c174b
mangle tag bound declarations properly

diff -r 6f29df8d2007 -r 2c1fc7b29c9c src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Fri Aug 26 00:05:45 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Fri Aug 26 00:19:25 2011 +0200
@@ -1671,8 +1671,7 @@
       else if should_generate_tag_bound_decl ctxt mono type_enc universal T then
         let
           val var = ATerm (name, [])
-          val tagged_var =
-            ATerm (type_tag, [ho_term_from_typ format type_enc T, var])
+          val tagged_var = var |> tag_with_type ctxt format mono type_enc pos T
         in SOME (AAtom (ATerm (`I tptp_equal, [tagged_var, var]))) end
       else
         NONE