src/HOL/Tools/ATP/atp_problem_generate.ML

     val app =
       IConst (app_op, head_T --> head_T, [arg_T, res_T])
       |> mangle_type_args_in_iterm format type_enc
   in list_app app [head, arg] end
 
-fun firstorderize_fact thy monom_constrs format type_enc app_op_aliases
-                       sym_tab =
+fun firstorderize_fact thy monom_constrs format type_enc sym_tab
+                       app_op_aliases =
   let
     fun do_app arg head = do_app_op format type_enc head arg
     fun list_app_ops head args = fold do_app args head
     fun introduce_app_ops tm =
       let val (head, args) = tm |> strip_iterm_comb ||> map introduce_app_ops in

     val sym_tab = sym_table_for_facts ctxt type_enc app_op_level conjs facts
     val mono = conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc
     val (polym_constrs, monom_constrs) =
       all_constrs_of_polymorphic_datatypes thy
       |>> map (make_fixed_const (SOME format))
-    val firstorderize =
-      firstorderize_fact thy monom_constrs format type_enc app_op_aliases
-                         sym_tab
-    val (conjs, facts) = (conjs, facts) |> pairself (map firstorderize)
+    fun firstorderize in_helper =
+      firstorderize_fact thy monom_constrs format type_enc sym_tab
+                         (app_op_aliases andalso not in_helper)
+    val (conjs, facts) = (conjs, facts) |> pairself (map (firstorderize false))
     val sym_tab = sym_table_for_facts ctxt type_enc Incomplete_Apply conjs facts
     val helpers =
       sym_tab |> helper_facts_for_sym_table ctxt format type_enc
-              |> map firstorderize
+              |> map (firstorderize true)
     val mono_Ts =
       helpers @ conjs @ facts |> monotonic_types_for_facts ctxt mono type_enc
     val class_decl_lines = decl_lines_for_classes type_enc classes
     val (app_op_alias_eq_tms, app_op_alias_eq_lines) =
       app_op_alias_lines_for_sym_table ctxt monom_constrs format conj_sym_kind