src/HOL/Tools/ATP/atp_problem_generate.ML

   case polymorphism_of_type_enc type_enc of
     Raw_Polymorphic _ => true
   | Type_Class_Polymorphic => true
   | _ => false
 
+fun is_type_enc_mangling type_enc =
+  polymorphism_of_type_enc type_enc = Mangled_Monomorphic
+
 fun level_of_type_enc (Native (_, _, level)) = level
   | level_of_type_enc (Guards (_, level)) = level
   | level_of_type_enc (Tags (_, level)) = level
 
 fun is_type_level_uniform (Nonmono_Types (_, Non_Uniform)) = false

     else x :: filter_out (type_generalization thy T o get_T) xs
   end
 
 (* The Booleans indicate whether all type arguments should be kept. *)
 datatype type_arg_policy =
-  Mangled_Type_Args | (* ### TODO: get rid of this *)
   All_Type_Args |
   Noninfer_Type_Args |
   Constr_Infer_Type_Args |
   No_Type_Args
 
 fun type_arg_policy constrs type_enc s =
   let val poly = polymorphism_of_type_enc type_enc in
-    if s = type_tag_name then
-      if poly = Mangled_Monomorphic then Mangled_Type_Args else All_Type_Args
+    if s = type_tag_name then (* ### FIXME: why not "type_guard_name" as well? *)
+      All_Type_Args
     else case type_enc of
       Native (_, Raw_Polymorphic _, _) => All_Type_Args
     | Native (_, Type_Class_Polymorphic, _) => All_Type_Args
     | _ =>
       let val level = level_of_type_enc type_enc in
         if level = No_Types orelse s = @{const_name HOL.eq} orelse
            (case level of Const_Types _ => s = app_op_name | _ => false) then
           No_Type_Args
         else if poly = Mangled_Monomorphic then
-          Mangled_Type_Args
+          All_Type_Args
         else if level = All_Types then
           case type_enc of
             Guards _ => Noninfer_Type_Args
           | Tags _ => No_Type_Args
         else if level = Undercover_Types then

 
 fun mangle_type_args_in_const type_enc (name as (s, _)) T_args =
   case unprefix_and_unascii const_prefix s of
     NONE => (name, T_args)
   | SOME s'' =>
-    case type_arg_policy [] type_enc (invert_const s'') of
-      Mangled_Type_Args => (mangled_const_name type_enc T_args name, [])
-    | _ => (name, T_args)
+    if is_type_enc_mangling type_enc then
+      (mangled_const_name type_enc T_args name, [])
+    else
+      (name, T_args)
 fun mangle_type_args_in_iterm type_enc =
-  if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
+  if is_type_enc_mangling type_enc then
     let
       fun mangle (IApp (tm1, tm2)) = IApp (mangle tm1, mangle tm2)
         | mangle (tm as IConst (_, _, [])) = tm
         | mangle (IConst (name, T, T_args)) =
           mangle_type_args_in_const type_enc name T_args

       if level_of_type_enc type_enc = No_Types orelse s = tptp_choice then []
       else T_args
     | SOME s'' =>
       let val s'' = invert_const s'' in
         case type_arg_policy constrs type_enc s'' of
-          Mangled_Type_Args => raise Fail "unexpected (un)mangled symbol"
-        | All_Type_Args => T_args
+          All_Type_Args => T_args
         | Noninfer_Type_Args =>
           filter_type_args (not o fst) thy s'' (chop_fun ary) T_args
         | Constr_Infer_Type_Args =>
           filter_type_args fst thy s'' strip_type T_args
         | No_Type_Args => []

     fun add_undefined_const T =
       let
         (* FIXME: make sure type arguments are filtered / clean up code *)
         val (s, s') =
           `(make_fixed_const NONE) @{const_name undefined}
-          |> (case type_arg_policy [] type_enc @{const_name undefined} of
-                Mangled_Type_Args => mangled_const_name type_enc [T]
-              | _ => I)
+          |> (is_type_enc_mangling type_enc ? mangled_const_name type_enc [T])
       in
         Symtab.map_default (s, [])
                            (insert_type thy #3 (s', [T], T, false, 0, false))
       end
     fun add_TYPE_const () =