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))