# HG changeset patch # User blanchet # Date 1450551771 -3600 # Node ID 2ce3d12015b3309ee2a0882ad13b4b4f2ba5b2fe # Parent edceda92a43520b37e0df46ba88ee14ecc3dd6c6 cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer diff -r edceda92a435 -r 2ce3d12015b3 src/HOL/TPTP/atp_problem_import.ML --- a/src/HOL/TPTP/atp_problem_import.ML Sat Dec 19 20:02:51 2015 +0100 +++ b/src/HOL/TPTP/atp_problem_import.ML Sat Dec 19 20:02:51 2015 +0100 @@ -315,6 +315,7 @@ | "DFG" => (DFG Monomorphic, "mono_native", liftingN) | _ => error ("Unknown format " ^ quote format_str ^ " (expected \"FOF\", \"TF0\", \"TH0\", or \"DFG\")")) + val generate_info = false val uncurried_aliases = false val readable_names = true val presimp = true @@ -322,7 +323,8 @@ map (apfst (rpair (Global, Non_Rec_Def))) defs @ map (apfst (rpair (Global, General))) nondefs val (atp_problem, _, _, _) = - generate_atp_problem ctxt format Hypothesis (type_enc_of_string Strict type_enc) Translator + generate_atp_problem ctxt generate_info format Hypothesis (type_enc_of_string Strict type_enc) + Translator lam_trans uncurried_aliases readable_names presimp [] conj facts val ord = effective_term_order ctxt spassN diff -r edceda92a435 -r 2ce3d12015b3 src/HOL/TPTP/atp_theory_export.ML --- a/src/HOL/TPTP/atp_theory_export.ML Sat Dec 19 20:02:51 2015 +0100 +++ b/src/HOL/TPTP/atp_theory_export.ML Sat Dec 19 20:02:51 2015 +0100 @@ -75,12 +75,11 @@ | SOME failure => string_of_atp_failure failure)) in outcome end -fun is_problem_line_reprovable ctxt format prelude axioms deps - (Formula (ident', _, phi, _, _)) = +fun is_problem_line_reprovable ctxt format prelude axioms deps (Formula (ident', _, phi, _, _)) = is_none (run_atp ctxt format - ((factsN, Formula (ident', Conjecture, phi, NONE, []) :: - map_filter (Symtab.lookup axioms) deps) :: - prelude)) + ((factsN, + Formula (ident', Conjecture, phi, NONE, []) :: map_filter (Symtab.lookup axioms) deps) :: + prelude)) | is_problem_line_reprovable _ _ _ _ _ _ = false fun inference_term _ [] = NONE @@ -93,7 +92,7 @@ |> SOME fun add_inferences_to_problem_line ctxt format check_infs prelude axioms infers - (line as Formula ((ident, alt), Axiom, phi, NONE, tms)) = + (line as Formula ((ident, alt), Axiom, phi, NONE, info)) = let val deps = case these (AList.lookup (op =) infers ident) of @@ -106,7 +105,7 @@ else deps in - Formula ((ident, alt), Lemma, phi, inference_term check_infs deps, tms) + Formula ((ident, alt), Lemma, phi, inference_term check_infs deps, info) end | add_inferences_to_problem_line _ _ _ _ _ _ line = line @@ -170,7 +169,7 @@ facts |> map (fn ((_, loc), th) => ((Thm.get_name_hint th, loc), th |> Thm.prop_of |> mono ? monomorphize_term ctxt)) - |> generate_atp_problem ctxt format Axiom type_enc Exporter combsN false false true [] + |> generate_atp_problem ctxt true format Axiom type_enc Exporter combsN false false true [] @{prop False} |> #1 |> sort_by (heading_sort_key o fst) val prelude = fst (split_last problem) @@ -269,13 +268,13 @@ val hol_base_name = encode_meta "HOL" fun should_generate_problem thy base_name (Formula ((_, alt), _, _, _, _)) = - case try (Global_Theory.get_thm thy) alt of + (case try (Global_Theory.get_thm thy) alt of SOME th => - (* This is a crude hack to detect theorems stated and proved by the user (as - opposed to those derived by various packages). In addition, we leave out - everything in "HOL" as too basic to be interesting. *) + (* This is a crude hack to detect theorems stated and proved by the user (as opposed to those + derived by various packages). In addition, we leave out everything in "HOL" as too basic to + be interesting. *) Thm.legacy_get_kind th <> "" andalso base_name <> hol_base_name - | NONE => false + | NONE => false) (* Convention: theoryname__goalname *) fun problem_name_of base_name n alt = @@ -342,13 +341,12 @@ | write_problem_files n seen_facts includes seen_ss ((base_name, fact_line :: fact_lines) :: groups) = let - val (ident, alt, pname, sname, conj) = + val (alt, pname, sname, conj) = (case fact_line of Formula ((ident, alt), _, phi, _, _) => - (ident, alt, problem_name_of base_name n (encode_meta alt), + (alt, problem_name_of base_name n (encode_meta alt), suggestion_name_of base_name n (encode_meta alt), Formula ((ident, alt), Conjecture, phi, NONE, []))) - val fact = the (Symtab.lookup fact_tab alt) val fact_s = tptp_string_of_line format fact_line in diff -r edceda92a435 -r 2ce3d12015b3 src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Sat Dec 19 20:02:51 2015 +0100 +++ b/src/HOL/Tools/ATP/atp_problem.ML Sat Dec 19 20:02:51 2015 +0100 @@ -98,7 +98,7 @@ val tptp_empty_list : string val dfg_individual_type : string val isabelle_info_prefix : string - val isabelle_info : string -> int -> (string, 'a) atp_term list + val isabelle_info : bool -> string -> int -> (string, 'a) atp_term list val extract_isabelle_status : (string, 'a) atp_term list -> string option val extract_isabelle_rank : (string, 'a) atp_term list -> int val inductionN : string @@ -138,6 +138,7 @@ ('c -> 'e) -> ('a, 'b, 'c, 'd) atp_formula -> ('a, 'b, 'e, 'd) atp_formula val strip_atype : 'a atp_type -> 'a list * ('a atp_type list * 'a atp_type) val is_format_higher_order : atp_format -> bool + val tptp_string_of_format : atp_format -> string val tptp_string_of_line : atp_format -> string atp_problem_line -> string val lines_of_atp_problem : atp_format -> term_order -> (unit -> (string * int) list) @@ -271,12 +272,16 @@ val default_rank = 1000 val default_term_order_weight = 1 -(* Currently, only SPASS 3.8ds can process Isabelle metainformation. *) -fun isabelle_info status rank = - [] |> rank <> default_rank - ? cons (ATerm ((isabelle_info_prefix ^ rankN, []), - [ATerm ((string_of_int rank, []), [])])) - |> status <> "" ? cons (ATerm ((isabelle_info_prefix ^ status, []), [])) +(* Currently, only SPASS 3.8ds and (to a lesser extent) Metis can process Isabelle + metainformation. *) +fun isabelle_info generate_info status rank = + if generate_info then + [] |> rank <> default_rank + ? cons (ATerm ((isabelle_info_prefix ^ rankN, []), + [ATerm ((string_of_int rank, []), [])])) + |> status <> "" ? cons (ATerm ((isabelle_info_prefix ^ status, []), [])) + else + [] fun extract_isabelle_status (ATerm ((s, []), []) :: _) = try (unprefix isabelle_info_prefix) s @@ -542,13 +547,16 @@ | tptp_string_of_line format (Sym_Decl (ident, sym, ty)) = tptp_string_of_format format ^ "(" ^ ident ^ ", type,\n " ^ sym ^ " : " ^ string_of_type format ty ^ ").\n" - | tptp_string_of_line format (Formula ((ident, alt), kind, phi, source, _)) = + | tptp_string_of_line format (Formula ((ident, alt), kind, phi, source, info)) = tptp_string_of_format format ^ "(" ^ ident ^ ", " ^ tptp_string_of_role kind ^ "," ^ "\n (" ^ tptp_string_of_formula format phi ^ ")" ^ (case source of SOME tm => ", " ^ tptp_string_of_term format tm - | NONE => "") ^ + | NONE => if null info then "" else ", []") ^ + (case info of + [] => "" + | tms => ", [" ^ commas (map (tptp_string_of_term format) tms) ^ "]") ^ ")." ^ maybe_alt alt ^ "\n" fun tptp_lines format = diff -r edceda92a435 -r 2ce3d12015b3 src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Sat Dec 19 20:02:51 2015 +0100 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Sat Dec 19 20:02:51 2015 +0100 @@ -112,9 +112,10 @@ Proof.context -> type_enc -> string -> term list -> term list * term list val string_of_status : status -> string val factsN : string - val generate_atp_problem : Proof.context -> atp_format -> atp_formula_role -> type_enc -> mode -> - string -> bool -> bool -> bool -> term list -> term -> ((string * stature) * term) list -> - string atp_problem * string Symtab.table * (string * term) list * int Symtab.table + val generate_atp_problem : Proof.context -> bool -> atp_format -> atp_formula_role -> type_enc -> + mode -> string -> bool -> bool -> bool -> term list -> term -> + ((string * stature) * term) list -> string atp_problem * string Symtab.table + * (string * term) list * int Symtab.table val atp_problem_selection_weights : string atp_problem -> (string * real) list val atp_problem_term_order_info : string atp_problem -> (string * int) list end; @@ -2017,7 +2018,7 @@ (* Each fact is given a unique fact number to avoid name clashes (e.g., because of monomorphization). The TPTP forbids name clashes, and some of the remote provers might care. *) -fun line_of_fact ctxt prefix encode alt freshen pos mono type_enc rank +fun line_of_fact ctxt generate_info prefix encode alt freshen pos mono type_enc rank (j, {name, stature = (_, status), role, iformula, atomic_types}) = Formula ((prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name, alt name), @@ -2027,23 +2028,22 @@ should_guard_var_in_formula (if pos then SOME true else NONE) |> close_formula_universally |> bound_tvars type_enc true atomic_types, - NONE, isabelle_info (string_of_status status) (rank j)) + NONE, isabelle_info generate_info (string_of_status status) (rank j)) -fun lines_of_subclass type_enc sub super = +fun lines_of_subclass generate_info type_enc sub super = Formula ((subclass_prefix ^ ascii_of sub ^ "___" ^ ascii_of super, ""), Axiom, AConn (AImplies, [sub, super] |> map (fn s => class_atom type_enc (s, tvar_a))) |> bound_tvars type_enc false [tvar_a], - NONE, isabelle_info inductiveN helper_rank) + NONE, isabelle_info generate_info inductiveN helper_rank) -fun lines_of_subclass_pair type_enc (sub, supers) = +fun lines_of_subclass_pair generate_info type_enc (sub, supers) = if polymorphism_of_type_enc type_enc = Type_Class_Polymorphic then - [Class_Decl (class_decl_prefix ^ ascii_of sub, `make_class sub, - map (`make_class) supers)] + [Class_Decl (class_decl_prefix ^ ascii_of sub, `make_class sub, map (`make_class) supers)] else - map (lines_of_subclass type_enc sub) supers + map (lines_of_subclass generate_info type_enc sub) supers -fun line_of_tcon_clause type_enc (name, prems, (cl, T)) = +fun line_of_tcon_clause generate_info type_enc (name, prems, (cl, T)) = if polymorphism_of_type_enc type_enc = Type_Class_Polymorphic then Class_Memb (class_memb_prefix ^ name, map (fn (cls, T) => (T |> dest_TVar |> tvar_name, map (`make_class) cls)) prems, @@ -2053,14 +2053,12 @@ mk_ahorn (maps (class_atoms type_enc) prems) (class_atom type_enc (cl, T)) |> bound_tvars type_enc true (snd (dest_Type T)), - NONE, isabelle_info inductiveN helper_rank) + NONE, isabelle_info generate_info inductiveN helper_rank) -fun line_of_conjecture ctxt mono type_enc - ({name, role, iformula, atomic_types, ...} : ifact) = +fun line_of_conjecture ctxt mono type_enc ({name, role, iformula, atomic_types, ...} : ifact) = Formula ((conjecture_prefix ^ name, ""), role, iformula - |> formula_of_iformula ctxt mono type_enc - should_guard_var_in_formula (SOME false) + |> formula_of_iformula ctxt mono type_enc should_guard_var_in_formula (SOME false) |> close_formula_universally |> bound_tvars type_enc true atomic_types, NONE, []) @@ -2230,7 +2228,7 @@ ? fold (add_fact_monotonic_types ctxt mono type_enc) facts end -fun line_of_guards_mono_type ctxt mono type_enc T = +fun line_of_guards_mono_type ctxt generate_info mono type_enc T = Formula ((guards_sym_formula_prefix ^ ascii_of (mangled_type type_enc T), ""), Axiom, IConst (`make_bound_var "X", T, []) @@ -2240,21 +2238,21 @@ (SOME true) |> close_formula_universally |> bound_tvars type_enc true (atomic_types_of T), - NONE, isabelle_info inductiveN helper_rank) + NONE, isabelle_info generate_info inductiveN helper_rank) -fun line_of_tags_mono_type ctxt mono type_enc T = +fun line_of_tags_mono_type ctxt generate_info mono type_enc T = let val x_var = ATerm ((`make_bound_var "X", []), []) in Formula ((tags_sym_formula_prefix ^ ascii_of (mangled_type type_enc T), ""), Axiom, eq_formula type_enc (atomic_types_of T) [] false (tag_with_type ctxt mono type_enc NONE T x_var) x_var, - NONE, isabelle_info non_rec_defN helper_rank) + NONE, isabelle_info generate_info non_rec_defN helper_rank) end -fun lines_of_mono_types ctxt mono type_enc = +fun lines_of_mono_types ctxt generate_info mono type_enc = (case type_enc of Native _ => K [] - | Guards _ => map (line_of_guards_mono_type ctxt mono type_enc) - | Tags _ => map (line_of_tags_mono_type ctxt mono type_enc)) + | Guards _ => map (line_of_guards_mono_type ctxt generate_info mono type_enc) + | Tags _ => map (line_of_tags_mono_type ctxt generate_info mono type_enc)) fun decl_line_of_sym ctxt mono type_enc s (s', T_args, T, pred_sym, ary, _) = let @@ -2280,8 +2278,8 @@ fun honor_conj_sym_role in_conj = (if in_conj then Hypothesis else Axiom, I) -fun line_of_guards_sym_decl ctxt mono type_enc n s j - (s', T_args, T, _, ary, in_conj) = +fun line_of_guards_sym_decl ctxt generate_info mono type_enc n s j + (s', T_args, T, _, ary, in_conj) = let val thy = Proof_Context.theory_of ctxt val (role, maybe_negate) = honor_conj_sym_role in_conj @@ -2310,11 +2308,11 @@ |> close_formula_universally |> bound_tvars type_enc (n > 1) (atomic_types_of T) |> maybe_negate, - NONE, isabelle_info inductiveN helper_rank) + NONE, isabelle_info generate_info inductiveN helper_rank) end -fun lines_of_tags_sym_decl ctxt mono type_enc n s - (j, (s', T_args, T, pred_sym, ary, in_conj)) = +fun lines_of_tags_sym_decl ctxt generate_info mono type_enc n s + (j, (s', T_args, T, pred_sym, ary, in_conj)) = let val thy = Proof_Context.theory_of ctxt val level = level_of_type_enc type_enc @@ -2330,7 +2328,7 @@ val tag_with = tag_with_type ctxt mono type_enc NONE fun formula c = [Formula ((ident, ""), role, eq (tag_with res_T c) c, NONE, - isabelle_info non_rec_defN helper_rank)] + isabelle_info generate_info non_rec_defN helper_rank)] in if pred_sym orelse not (should_encode_type ctxt mono level res_T) then [] @@ -2355,7 +2353,7 @@ end | rationalize_decls _ decls = decls -fun lines_of_sym_decls ctxt mono type_enc (s, decls) = +fun lines_of_sym_decls ctxt generate_info mono type_enc (s, decls) = (case type_enc of Native _ => [decl_line_of_sym ctxt mono type_enc s (hd decls)] | Guards (_, level) => @@ -2365,21 +2363,23 @@ val n = length decls val decls = decls |> filter (should_encode_type ctxt mono level o result_type_of_decl) in - (0 upto length decls - 1, decls) |-> map2 (line_of_guards_sym_decl ctxt mono type_enc n s) + (0 upto length decls - 1, decls) + |-> map2 (line_of_guards_sym_decl ctxt generate_info mono type_enc n s) end | Tags (_, level) => if is_type_level_uniform level then [] else let val n = length decls in - (0 upto n - 1 ~~ decls) |> maps (lines_of_tags_sym_decl ctxt mono type_enc n s) + (0 upto n - 1 ~~ decls) + |> maps (lines_of_tags_sym_decl ctxt generate_info mono type_enc n s) end) -fun lines_of_sym_decl_table ctxt mono type_enc mono_Ts sym_decl_tab = +fun lines_of_sym_decl_table ctxt generate_info mono type_enc mono_Ts sym_decl_tab = let val syms = sym_decl_tab |> Symtab.dest |> sort_by fst - val mono_lines = lines_of_mono_types ctxt mono type_enc mono_Ts - val decl_lines = maps (lines_of_sym_decls ctxt mono type_enc) syms + val mono_lines = lines_of_mono_types ctxt generate_info mono type_enc mono_Ts + val decl_lines = maps (lines_of_sym_decls ctxt generate_info mono type_enc) syms in mono_lines @ decl_lines end fun datatypes_of_sym_table ctxt ctrss (DFG Polymorphic) (type_enc as Native _) uncurried_aliases @@ -2426,8 +2426,8 @@ fun pair_append (xs1, xs2) (ys1, ys2) = (xs1 @ ys1, xs2 @ ys2) -fun do_uncurried_alias_lines_of_sym ctxt ctrss mono type_enc sym_tab0 sym_tab - base_s0 types in_conj = +fun do_uncurried_alias_lines_of_sym ctxt generate_info ctrss mono type_enc sym_tab0 sym_tab base_s0 + types in_conj = let fun do_alias ary = let @@ -2464,31 +2464,32 @@ in ([tm1, tm2], [Formula ((uncurried_alias_eq_prefix ^ s2, ""), role, eq |> maybe_negate, NONE, - isabelle_info non_rec_defN helper_rank)]) + isabelle_info generate_info non_rec_defN helper_rank)]) |> (if ary - 1 = base_ary orelse Symtab.defined sym_tab s1 then I else pair_append (do_alias (ary - 1))) end in do_alias end -fun uncurried_alias_lines_of_sym ctxt ctrss mono type_enc sym_tab0 sym_tab +fun uncurried_alias_lines_of_sym ctxt generate_info ctrss mono type_enc sym_tab0 sym_tab (s, {min_ary, types, in_conj, ...} : sym_info) = (case unprefix_and_unascii const_prefix s of SOME mangled_s => if String.isSubstring uncurried_alias_sep mangled_s then let val base_s0 = mangled_s |> unmangled_invert_const in - do_uncurried_alias_lines_of_sym ctxt ctrss mono type_enc sym_tab0 sym_tab base_s0 types - in_conj min_ary + do_uncurried_alias_lines_of_sym ctxt generate_info ctrss mono type_enc sym_tab0 sym_tab + base_s0 types in_conj min_ary end else ([], []) | NONE => ([], [])) -fun uncurried_alias_lines_of_sym_table ctxt ctrss mono type_enc uncurried_aliases sym_tab0 sym_tab = +fun uncurried_alias_lines_of_sym_table ctxt generate_info ctrss mono type_enc uncurried_aliases + sym_tab0 sym_tab = ([], []) |> uncurried_aliases - ? Symtab.fold_rev - (pair_append o uncurried_alias_lines_of_sym ctxt ctrss mono type_enc sym_tab0 sym_tab) - sym_tab + ? Symtab.fold_rev (pair_append + o uncurried_alias_lines_of_sym ctxt generate_info ctrss mono type_enc sym_tab0 sym_tab) + sym_tab val implicit_declsN = "Could-be-implicit typings" val explicit_declsN = "Explicit typings" @@ -2563,8 +2564,8 @@ val app_op_and_predicator_threshold = 45 -fun generate_atp_problem ctxt format prem_role type_enc mode lam_trans uncurried_aliases - readable_names presimp hyp_ts concl_t facts = +fun generate_atp_problem ctxt generate_info format prem_role type_enc mode lam_trans + uncurried_aliases readable_names presimp hyp_ts concl_t facts = let val thy = Proof_Context.theory_of ctxt val type_enc = type_enc |> adjust_type_enc format @@ -2595,7 +2596,8 @@ val (ho_stuff, sym_tab) = sym_table_of_facts ctxt type_enc Min_App_Op conjs facts val (uncurried_alias_eq_tms, uncurried_alias_eq_lines) = - uncurried_alias_lines_of_sym_table ctxt ctrss mono type_enc uncurried_aliases sym_tab0 sym_tab + uncurried_alias_lines_of_sym_table ctxt generate_info ctrss mono type_enc uncurried_aliases + sym_tab0 sym_tab val (_, sym_tab) = (ho_stuff, sym_tab) |> fold (add_iterm_syms_to_sym_table ctxt Min_App_Op false false) @@ -2610,7 +2612,7 @@ val sym_decl_lines = (conjs, helpers @ facts, uncurried_alias_eq_tms) |> sym_decl_table_of_facts thy type_enc sym_tab - |> lines_of_sym_decl_table ctxt mono type_enc mono_Ts + |> lines_of_sym_decl_table ctxt generate_info mono type_enc mono_Ts val datatype_decl_lines = map decl_line_of_datatype datatypes val decl_lines = class_decl_lines @ sym_decl_lines @ datatype_decl_lines val num_facts = length facts @@ -2618,13 +2620,14 @@ val pos = mode <> Exporter val rank_of = rank_of_fact_num num_facts val fact_lines = - map (line_of_fact ctxt fact_prefix ascii_of I freshen pos mono type_enc rank_of) + map (line_of_fact ctxt generate_info fact_prefix ascii_of I freshen pos mono type_enc rank_of) (0 upto num_facts - 1 ~~ facts) - val subclass_lines = maps (lines_of_subclass_pair type_enc) subclass_pairs - val tcon_lines = map (line_of_tcon_clause type_enc) tcon_clauses + val subclass_lines = maps (lines_of_subclass_pair generate_info type_enc) subclass_pairs + val tcon_lines = map (line_of_tcon_clause generate_info type_enc) tcon_clauses val helper_lines = 0 upto length helpers - 1 ~~ helpers - |> map (line_of_fact ctxt helper_prefix I (K "") false true mono type_enc (K default_rank)) + |> map (line_of_fact ctxt generate_info helper_prefix I (K "") false true mono type_enc + (K default_rank)) val free_type_lines = lines_of_free_types type_enc (facts @ conjs) val conj_lines = map (line_of_conjecture ctxt mono type_enc) conjs (* Reordering these might confuse the proof reconstruction code. *) diff -r edceda92a435 -r 2ce3d12015b3 src/HOL/Tools/Metis/metis_generate.ML --- a/src/HOL/Tools/Metis/metis_generate.ML Sat Dec 19 20:02:51 2015 +0100 +++ b/src/HOL/Tools/Metis/metis_generate.ML Sat Dec 19 20:02:51 2015 +0100 @@ -227,7 +227,7 @@ *) val lam_trans = if lam_trans = combsN then no_lamsN else lam_trans val (atp_problem, _, lifted, sym_tab) = - generate_atp_problem ctxt CNF Hypothesis type_enc Metis lam_trans false false false [] + generate_atp_problem ctxt true CNF Hypothesis type_enc Metis lam_trans false false false [] @{prop False} props (* val _ = tracing ("ATP PROBLEM: " ^ diff -r edceda92a435 -r 2ce3d12015b3 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Sat Dec 19 20:02:51 2015 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Sat Dec 19 20:02:51 2015 +0100 @@ -235,6 +235,7 @@ val num_facts = Real.ceil (max_fact_factor * Real.fromInt best_max_facts) + max_fact_factor_fudge |> Integer.min (length facts) + val generate_info = (case format of DFG _ => true | _ => false) val strictness = if strict then Strict else Non_Strict val type_enc = type_enc |> choose_type_enc strictness best_type_enc format val sound = is_type_enc_sound type_enc @@ -273,8 +274,8 @@ generate_waldmeister_problem ctxt hyp_ts concl_t #> (fn (a, b, c, d, e) => (a, b, c, d, SOME e)) else - generate_atp_problem ctxt format prem_role type_enc atp_mode lam_trans - uncurried_aliases readable_names true hyp_ts concl_t + generate_atp_problem ctxt generate_info format prem_role type_enc atp_mode + lam_trans uncurried_aliases readable_names true hyp_ts concl_t #> (fn (a, b, c, d) => (a, b, c, d, NONE))) fun sel_weights () = atp_problem_selection_weights atp_problem