src/HOL/Tools/ATP/atp_translate.ML

        case try_unsuffixes ats s of
          SOME s => (constr Arg_Light, s)
        | NONE => (constr Heavy, s))
   | NONE => fallback s
 
+fun is_mangled_arg_light poly level =
+  poly = Mangled_Monomorphic andalso heaviness_of_level level = Arg_Light
+
 fun type_enc_from_string soundness s =
   (case try (unprefix "poly_") s of
      SOME s => (SOME Polymorphic, s)
    | NONE =>
      case try (unprefix "raw_mono_") s of

               if heaviness_of_level level = Heavy then
                 Simple_Types (Higher_Order, Mangled_Monomorphic, level)
               else
                 raise Same.SAME
             | _ => raise Same.SAME)
-         | ("guards", (SOME poly, _)) => Guards (poly, level)
-         | ("tags", (SOME Polymorphic, _)) => Tags (Polymorphic, level)
-         | ("tags", (SOME poly, _)) => Tags (poly, level)
+         | ("guards", (SOME poly, _)) =>
+           if is_mangled_arg_light poly level then raise Same.SAME
+           else Guards (poly, level)
+         | ("tags", (SOME poly, _)) =>
+           if is_mangled_arg_light poly level then raise Same.SAME
+           else Tags (poly, level)
          | ("args", (SOME poly, All_Types (* naja *))) =>
            Guards (poly, Const_Arg_Types)
          | ("erased", (NONE, All_Types (* naja *))) =>
            Guards (Polymorphic, No_Types)
          | _ => raise Same.SAME)