src/HOL/Tools/ATP/atp_problem.ML

      | _ => ty)
   | flatten_type (ty as AType _) = ty
   | flatten_type _ =
     raise Fail "unexpected higher-order type in first-order format"
 
-val dfg_individual_type = "i" (* shouldn't clash *)
+val dfg_individual_type = "ii" (* cannot clash *)
 
 fun str_for_type format ty =
   let
     val dfg = (format = DFG DFG_Sorted)
     fun str _ (AType (s, [])) =