src/HOL/Tools/ATP/atp_problem_generate.ML

           (case (poly, level) of
             (_, Nonmono_Types _) => raise Same.SAME
           | (_, Undercover_Types) => raise Same.SAME
           | (Mangled_Monomorphic, _) =>
             if is_type_level_uniform level then
-              Native (Higher_Order THF_With_Choice, Without_FOOL, Mangled_Monomorphic, level)
+              Native (Higher_Order THF_With_Choice, fool, Mangled_Monomorphic, level)
             else
               raise Same.SAME
            | (poly as Raw_Polymorphic _, All_Types) =>
-             Native (Higher_Order THF_With_Choice, Without_FOOL, poly, All_Types)
+             Native (Higher_Order THF_With_Choice, fool, poly, All_Types)
            | _ => raise Same.SAME))
       end
 
     fun nonnative_of_string core =
       (case (core, poly, level) of