src/HOL/Tools/ATP/atp_translate.ML

                     (Simple_Types (order, _, level)) =
     Simple_Types (order, Mangled_Monomorphic, level)
   | adjust_type_enc (THF _) type_enc = type_enc
   | adjust_type_enc (TFF (TPTP_Monomorphic, _)) (Simple_Types (_, _, level)) =
     Simple_Types (First_Order, Mangled_Monomorphic, level)
-  | adjust_type_enc DFG_Sorted (Simple_Types (_, _, level)) =
+  | adjust_type_enc (DFG DFG_Sorted) (Simple_Types (_, _, level)) =
     Simple_Types (First_Order, Mangled_Monomorphic, level)
   | adjust_type_enc (TFF _) (Simple_Types (_, poly, level)) =
     Simple_Types (First_Order, poly, level)
   | adjust_type_enc format (Simple_Types (_, poly, level)) =
     adjust_type_enc format (Guards (poly, level))

             CNF => ensure_cnf_problem
           | CNF_UEQ => filter_cnf_ueq_problem
           | FOF => I
           | TFF (_, TPTP_Implicit) => I
           | THF (_, TPTP_Implicit, _) => I
+          | DFG DFG_Unsorted => I
           | _ => declare_undeclared_syms_in_atp_problem type_decl_prefix
                                                         implicit_declsN)
     val (problem, pool) = problem |> nice_atp_problem readable_names
     val helpers_offset = offset_of_heading_in_problem helpersN problem 0
     val typed_helpers =