1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Fri Jul 01 15:53:37 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Fri Jul 01 15:53:37 2011 +0200
     1.3 @@ -637,7 +637,10 @@
     1.4       (s = app_op_name andalso level_of_type_sys type_sys = Const_Arg_Types) then
     1.5      No_Type_Args
     1.6    else if s = type_tag_name then
     1.7 -    Explicit_Type_Args false
     1.8 +    (if polymorphism_of_type_sys type_sys = Mangled_Monomorphic then
     1.9 +       Mangled_Type_Args
    1.10 +     else
    1.11 +       Explicit_Type_Args) false
    1.12    else
    1.13      general_type_arg_policy type_sys
    1.14