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