# HG changeset patch
# User blanchet
# Date 1309528417 -7200
# Node ID e096b1effbbbdda87c33ef5d88e4734d77c61b72
# Parent  80673841372bd6acd9da007af0b4f9f11e9a0896
mangle "ti" tags

diff -r 80673841372b -r e096b1effbbb src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Fri Jul 01 15:53:37 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Fri Jul 01 15:53:37 2011 +0200
@@ -637,7 +637,10 @@
      (s = app_op_name andalso level_of_type_sys type_sys = Const_Arg_Types) then
     No_Type_Args
   else if s = type_tag_name then
-    Explicit_Type_Args false
+    (if polymorphism_of_type_sys type_sys = Mangled_Monomorphic then
+       Mangled_Type_Args
+     else
+       Explicit_Type_Args) false
   else
     general_type_arg_policy type_sys