1.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon Oct 14 11:14:14 2013 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Oct 15 10:59:34 2013 +0200
     1.3 @@ -1565,8 +1565,7 @@
     1.4                    end
     1.5                  | NONE =>
     1.6                    let
     1.7 -                    val pred_sym = top_level andalso not bool_vars
     1.8 -                    val ary =
     1.9 +                    val max_ary =
    1.10                        case unprefix_and_unascii const_prefix s of
    1.11                          SOME s =>
    1.12                          (if String.isSubstring uncurried_alias_sep s then
    1.13 @@ -1576,15 +1575,16 @@
    1.14                             SOME ary0 => Int.min (ary0, ary)
    1.15                           | NONE => ary)
    1.16                        | NONE => ary
    1.17 +                    val pred_sym = top_level andalso max_ary = ary andalso not bool_vars
    1.18                      val min_ary =
    1.19                        case app_op_level of
    1.20 -                        Min_App_Op => ary
    1.21 +                        Min_App_Op => max_ary
    1.22                        | Full_App_Op_And_Predicator => 0
    1.23 -                      | _ => fold (consider_var_ary T) fun_var_Ts ary
    1.24 +                      | _ => fold (consider_var_ary T) fun_var_Ts max_ary
    1.25                    in
    1.26                      Symtab.update_new (s,
    1.27                          {pred_sym = pred_sym, min_ary = min_ary,
    1.28 -                         max_ary = ary, types = [T], in_conj = conj_fact})
    1.29 +                         max_ary = max_ary, types = [T], in_conj = conj_fact})
    1.30                          sym_tab
    1.31                    end)
    1.32               end
    1.33 @@ -2750,12 +2750,10 @@
    1.34    else
    1.35      NONE
    1.36  
    1.37 -fun ctrss_of_descr descr =
    1.38 -  map_filter (ctrs_of_datatype descr) descr
    1.39 +fun ctrss_of_descr descr = map_filter (ctrs_of_datatype descr) descr
    1.40  
    1.41  fun all_ctrss_of_datatypes thy =
    1.42 -  Symtab.fold (snd #> #descr #> ctrss_of_descr #> append) (Datatype.get_all thy)
    1.43 -              []
    1.44 +  Symtab.fold (snd #> #descr #> ctrss_of_descr #> append) (Datatype.get_all thy) []
    1.45  
    1.46  val app_op_and_predicator_threshold = 45
    1.47  
    1.48 @@ -2765,35 +2763,26 @@
    1.49    let
    1.50      val thy = Proof_Context.theory_of ctxt
    1.51      val type_enc = type_enc |> adjust_type_enc format
    1.52 +    val exporter = (mode = Exporter)
    1.53 +    val completish = (mode = Sledgehammer_Completish)
    1.54      (* Forcing explicit applications is expensive for polymorphic encodings,
    1.55         because it takes only one existential variable ranging over "'a => 'b" to
    1.56         ruin everything. Hence we do it only if there are few facts (which is
    1.57         normally the case for "metis" and the minimizer). *)
    1.58      val app_op_level =
    1.59 -      if mode = Sledgehammer_Completish then
    1.60 +      if completish then
    1.61          Full_App_Op_And_Predicator
    1.62 -      else if length facts + length hyp_ts
    1.63 -              > app_op_and_predicator_threshold then
    1.64 -        if is_type_enc_polymorphic type_enc then Min_App_Op
    1.65 -        else Sufficient_App_Op
    1.66 +      else if length facts + length hyp_ts >= app_op_and_predicator_threshold then
    1.67 +        if is_type_enc_polymorphic type_enc then Min_App_Op else Sufficient_App_Op
    1.68        else
    1.69          Sufficient_App_Op_And_Predicator
    1.70 -    val exporter = (mode = Exporter)
    1.71 -    val completish = (mode = Sledgehammer_Completish)
    1.72      val lam_trans =
    1.73 -      if lam_trans = keep_lamsN andalso
    1.74 -         not (is_type_enc_higher_order type_enc) then
    1.75 -        liftingN
    1.76 -      else
    1.77 -        lam_trans
    1.78 -    val (fact_names, classes, conjs, facts, subclass_pairs, tcon_clauses,
    1.79 -         lifted) =
    1.80 -      translate_formulas ctxt prem_role format type_enc lam_trans preproc hyp_ts
    1.81 -                         concl_t facts
    1.82 -    val (_, sym_tab0) =
    1.83 -      sym_table_of_facts ctxt type_enc app_op_level conjs facts
    1.84 -    val mono =
    1.85 -      conjs @ facts |> mononotonicity_info_of_facts ctxt type_enc completish
    1.86 +      if lam_trans = keep_lamsN andalso not (is_type_enc_higher_order type_enc) then liftingN
    1.87 +      else lam_trans
    1.88 +    val (fact_names, classes, conjs, facts, subclass_pairs, tcon_clauses, lifted) =
    1.89 +      translate_formulas ctxt prem_role format type_enc lam_trans preproc hyp_ts concl_t facts
    1.90 +    val (_, sym_tab0) = sym_table_of_facts ctxt type_enc app_op_level conjs facts
    1.91 +    val mono = conjs @ facts |> mononotonicity_info_of_facts ctxt type_enc completish
    1.92      val ctrss = all_ctrss_of_datatypes thy
    1.93      fun firstorderize in_helper =
    1.94        firstorderize_fact thy ctrss type_enc