# HG changeset patch
# User blanchet
# Date 1311863559 -7200
# Node ID 2b75760fa75ea77d2f413b4b81a7b663e7f6a859
# Parent  ab4d8499815c3c9d55bb73be5c37e5cdc1bcc35b
no needless mangling

diff -r ab4d8499815c -r 2b75760fa75e src/HOL/Tools/ATP/atp_translate.ML
--- 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))