1.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Feb 02 12:42:05 2012 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Feb 02 12:42:05 2012 +0100
     1.3 @@ -1532,8 +1532,8 @@
     1.4        |> mangle_type_args_in_iterm format type_enc
     1.5    in list_app app [head, arg] end
     1.6  
     1.7 -fun firstorderize_fact thy monom_constrs format type_enc app_op_aliases
     1.8 -                       sym_tab =
     1.9 +fun firstorderize_fact thy monom_constrs format type_enc sym_tab
    1.10 +                       app_op_aliases =
    1.11    let
    1.12      fun do_app arg head = do_app_op format type_enc head arg
    1.13      fun list_app_ops head args = fold do_app args head
    1.14 @@ -2575,14 +2575,14 @@
    1.15      val (polym_constrs, monom_constrs) =
    1.16        all_constrs_of_polymorphic_datatypes thy
    1.17        |>> map (make_fixed_const (SOME format))
    1.18 -    val firstorderize =
    1.19 -      firstorderize_fact thy monom_constrs format type_enc app_op_aliases
    1.20 -                         sym_tab
    1.21 -    val (conjs, facts) = (conjs, facts) |> pairself (map firstorderize)
    1.22 +    fun firstorderize in_helper =
    1.23 +      firstorderize_fact thy monom_constrs format type_enc sym_tab
    1.24 +                         (app_op_aliases andalso not in_helper)
    1.25 +    val (conjs, facts) = (conjs, facts) |> pairself (map (firstorderize false))
    1.26      val sym_tab = sym_table_for_facts ctxt type_enc Incomplete_Apply conjs facts
    1.27      val helpers =
    1.28        sym_tab |> helper_facts_for_sym_table ctxt format type_enc
    1.29 -              |> map firstorderize
    1.30 +              |> map (firstorderize true)
    1.31      val mono_Ts =
    1.32        helpers @ conjs @ facts |> monotonic_types_for_facts ctxt mono type_enc
    1.33      val class_decl_lines = decl_lines_for_classes type_enc classes