no needless mangling

--- a/src/HOL/Tools/ATP/atp_translate.ML	Thu Jul 28 15:15:26 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Thu Jul 28 16:32:39 2011 +0200
@@ -1699,7 +1699,9 @@
       let
         val (s, s') =
           `make_fixed_const @{const_name undefined}
-          |> mangled_const_name format type_enc [T]
+          |> (case type_arg_policy type_enc @{const_name undefined} of
+                Mangled_Type_Args _ => mangled_const_name format type_enc [T]
+              | _ => I)
       in
         Symtab.map_default (s, [])
                            (insert_type ctxt #3 (s', [T], T, false, 0, false))