# HG changeset patch # User blanchet # Date 1402940459 -7200 # Node ID 2b6a96cc64c9e67e5a3ab183b346190478df1046 # Parent b2c629647a14de39e443a5f5e55e2b56d414878d simplified code diff -r b2c629647a14 -r 2b6a96cc64c9 src/HOL/ATP.thy --- a/src/HOL/ATP.thy Mon Jun 16 19:40:04 2014 +0200 +++ b/src/HOL/ATP.thy Mon Jun 16 19:40:59 2014 +0200 @@ -9,8 +9,8 @@ imports Meson begin -ML_file "Tools/lambda_lifting.ML" -ML_file "Tools/monomorph.ML" +subsection {* ATP problems and proofs *} + ML_file "Tools/ATP/atp_util.ML" ML_file "Tools/ATP/atp_problem.ML" ML_file "Tools/ATP/atp_proof.ML" @@ -137,8 +137,10 @@ eq_ac disj_comms disj_assoc conj_comms conj_assoc -subsection {* Setup *} +subsection {* Basic connection between ATPs and HOL *} +ML_file "Tools/lambda_lifting.ML" +ML_file "Tools/monomorph.ML" ML_file "Tools/ATP/atp_problem_generate.ML" ML_file "Tools/ATP/atp_proof_reconstruct.ML" ML_file "Tools/ATP/atp_systems.ML" diff -r b2c629647a14 -r 2b6a96cc64c9 src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Mon Jun 16 19:40:04 2014 +0200 +++ b/src/HOL/Sledgehammer.thy Mon Jun 16 19:40:59 2014 +0200 @@ -33,4 +33,8 @@ ML_file "Tools/Sledgehammer/sledgehammer.ML" ML_file "Tools/Sledgehammer/sledgehammer_commands.ML" +lemma "1 + 1 = (2::nat)" +sledgehammer [vampire, max_facts = 3] +oops + end diff -r b2c629647a14 -r 2b6a96cc64c9 src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Mon Jun 16 19:40:04 2014 +0200 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Mon Jun 16 19:40:59 2014 +0200 @@ -110,12 +110,9 @@ Proof.context -> type_enc -> string -> term list -> term list * term list val string_of_status : status -> string val factsN : string - val prepare_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 * stature) list vector - * (string * term) list * int Symtab.table + 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 atp_problem_selection_weights : string atp_problem -> (string * real) list val atp_problem_term_order_info : string atp_problem -> (string * int) list end; @@ -1279,8 +1276,7 @@ iformula_of_prop ctxt type_enc iff_for_eq (SOME (role <> Conjecture)) t [] |>> close_universally add_iterm_vars in - {name = name, stature = stature, role = role, iformula = iformula, - atomic_types = atomic_Ts} + {name = name, stature = stature, role = role, iformula = iformula, atomic_types = atomic_Ts} end fun is_format_with_defs (THF _) = true @@ -1295,7 +1291,7 @@ else Axiom in - (case t |> make_formula ctxt format type_enc iff_for_eq name stature role of + (case make_formula ctxt format type_enc iff_for_eq name stature role t of formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} => if s = tptp_true then NONE else SOME formula | formula => SOME formula) @@ -1303,13 +1299,10 @@ fun make_conjecture ctxt format type_enc = map (fn ((name, stature), (role, t)) => - let - val role = - if role <> Conjecture andalso is_legitimate_tptp_def t then Definition else role - in - t |> role = Conjecture ? s_not - |> make_formula ctxt format type_enc true name stature role - end) + let + val role' = if role <> Conjecture andalso is_legitimate_tptp_def t then Definition else role + val t' = t |> role' = Conjecture ? s_not + in make_formula ctxt format type_enc true name stature role' t' end) (** Finite and infinite type inference **) @@ -1907,10 +1900,8 @@ conjs |> make_conjecture ctxt format type_enc |> pull_and_reorder_definitions val facts = - facts |> map_filter (fn (name, (_, t)) => - make_fact ctxt format type_enc true (name, t)) + facts |> map_filter (fn (name, (_, t)) => make_fact ctxt format type_enc true (name, t)) |> pull_and_reorder_definitions - val fact_names = facts |> map (fn {name, stature, ...} : ifact => (name, stature)) val lifted = lam_facts |> map (extract_lambda_def o snd o snd) val lam_facts = lam_facts |> map_filter (make_fact ctxt format type_enc true o apsnd snd) val all_ts = concl_t :: hyp_ts @ fact_ts @@ -1922,8 +1913,7 @@ else make_tcon_clauses thy tycons supers val subclass_pairs = make_subclass_pairs thy subs supers in - (fact_names |> map single, union (op =) subs supers, conjs, - facts @ lam_facts, subclass_pairs, tcon_clauses, lifted) + (union (op =) subs supers, conjs, facts @ lam_facts, subclass_pairs, tcon_clauses, lifted) end val type_guard = `(make_fixed_const NONE) type_guard_name @@ -2616,7 +2606,7 @@ val app_op_and_predicator_threshold = 45 -fun prepare_atp_problem ctxt format prem_role type_enc mode lam_trans uncurried_aliases +fun generate_atp_problem ctxt 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 @@ -2636,7 +2626,7 @@ val lam_trans = if lam_trans = keep_lamsN andalso not (is_type_enc_higher_order type_enc) then liftingN else lam_trans - val (fact_names, classes, conjs, facts, subclass_pairs, tcon_clauses, lifted) = + val (classes, conjs, facts, subclass_pairs, tcon_clauses, lifted) = translate_formulas ctxt prem_role format type_enc lam_trans presimp hyp_ts concl_t facts val (_, sym_tab0) = sym_table_of_facts ctxt type_enc app_op_level conjs facts val mono = conjs @ facts |> mononotonicity_info_of_facts ctxt type_enc completish @@ -2700,8 +2690,8 @@ val (problem, pool) = problem |> nice_atp_problem readable_names format fun add_sym_ary (s, {min_ary, ...} : sym_info) = min_ary > 0 ? Symtab.insert (op =) (s, min_ary) in - (problem, pool |> Option.map snd |> the_default Symtab.empty, fact_names |> Vector.fromList, - lifted, Symtab.empty |> Symtab.fold add_sym_ary sym_tab) + (problem, Option.map snd pool |> the_default Symtab.empty, lifted, + Symtab.fold add_sym_ary sym_tab Symtab.empty) end (* FUDGE *) diff -r b2c629647a14 -r 2b6a96cc64c9 src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Mon Jun 16 19:40:04 2014 +0200 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Mon Jun 16 19:40:59 2014 +0200 @@ -38,10 +38,10 @@ bool -> int Symtab.table -> (string, string, (string, string atp_type) atp_term, string) atp_formula -> term - val used_facts_in_atp_proof : - Proof.context -> (string * stature) list vector -> string atp_proof -> (string * stature) list - val used_facts_in_unsound_atp_proof : Proof.context -> (string * stature) list vector -> - 'a atp_proof -> string list option + val used_facts_in_atp_proof : Proof.context -> (string * stature) list -> string atp_proof -> + (string * stature) list + val used_facts_in_unsound_atp_proof : Proof.context -> (string * stature) list -> 'a atp_proof -> + string list option val atp_proof_prefers_lifting : string atp_proof -> bool val is_typed_helper_used_in_atp_proof : string atp_proof -> bool val replace_dependencies_in_line : atp_step_name * atp_step_name list -> ('a, 'b) atp_step -> @@ -50,8 +50,8 @@ ATP_Problem_Generate.type_enc -> string Symtab.table -> (string * term) list -> int Symtab.table -> string atp_proof -> (term, string) atp_step list val introduce_spass_skolem : (term, string) atp_step list -> (term, string) atp_step list - val factify_atp_proof : (string * 'a) list vector -> term list -> term -> - (term, string) atp_step list -> (term, string) atp_step list + val factify_atp_proof : (string * 'a) list -> term list -> term -> (term, string) atp_step list -> + (term, string) atp_step list end; structure ATP_Proof_Reconstruct : ATP_PROOF_RECONSTRUCT = @@ -452,66 +452,58 @@ repair_tvar_sorts (do_formula true phi Vartab.empty) end -fun find_first_in_list_vector vec key = - Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key - | (_, value) => value) NONE vec - val unprefix_fact_number = space_implode "_" o tl o space_explode "_" -fun resolve_one_named_fact fact_names s = +fun resolve_fact facts s = (case try (unprefix fact_prefix) s of SOME s' => let val s' = s' |> unprefix_fact_number |> unascii_of in - s' |> find_first_in_list_vector fact_names |> Option.map (pair s') + AList.lookup (op =) facts s' |> Option.map (pair s') end | NONE => NONE) -fun resolve_fact fact_names = map_filter (resolve_one_named_fact fact_names) - -fun resolve_one_named_conjecture s = +fun resolve_conjecture s = (case try (unprefix conjecture_prefix) s of SOME s' => Int.fromString s' | NONE => NONE) -val resolve_conjecture = map_filter resolve_one_named_conjecture +fun resolve_facts facts = map_filter (resolve_fact facts) +val resolve_conjectures = map_filter resolve_conjecture fun is_axiom_used_in_proof pred = exists (fn ((_, ss), _, _, _, []) => exists pred ss | _ => false) -fun add_non_rec_defs fact_names accum = - Vector.foldl (fn (facts, facts') => - union (op =) (filter (fn (_, (_, status)) => status = Non_Rec_Def) facts) facts') - accum fact_names +fun add_non_rec_defs facts = + fold (fn fact as (_, (_, status)) => status = Non_Rec_Def ? insert (op =) fact) facts val leo2_extcnf_equal_neg_rule = "extcnf_equal_neg" val leo2_unfold_def_rule = "unfold_def" -fun add_fact ctxt fact_names ((_, ss), _, _, rule, deps) = +fun add_fact ctxt facts ((_, ss), _, _, rule, deps) = (if rule = leo2_extcnf_equal_neg_rule then insert (op =) (short_thm_name ctxt ext, (Global, General)) else if rule = leo2_unfold_def_rule then (* LEO 1.3.3 does not record definitions properly, leading to missing dependencies in the TSTP proof. Remove the next line once this is fixed. *) - add_non_rec_defs fact_names + add_non_rec_defs facts else if rule = agsyhol_core_rule orelse rule = satallax_core_rule then (fn [] => (* agsyHOL and Satallax don't include definitions in their unsatisfiable cores, so we assume the worst and include them all here. *) - [(short_thm_name ctxt ext, (Global, General))] |> add_non_rec_defs fact_names + [(short_thm_name ctxt ext, (Global, General))] |> add_non_rec_defs facts | facts => facts) else I) - #> (if null deps then union (op =) (resolve_fact fact_names ss) else I) + #> (if null deps then union (op =) (resolve_facts facts ss) else I) -fun used_facts_in_atp_proof ctxt fact_names atp_proof = - if null atp_proof then Vector.foldl (uncurry (union (op =))) [] fact_names - else fold (add_fact ctxt fact_names) atp_proof [] +fun used_facts_in_atp_proof ctxt facts atp_proof = + if null atp_proof then facts else fold (add_fact ctxt facts) atp_proof [] fun used_facts_in_unsound_atp_proof _ _ [] = NONE - | used_facts_in_unsound_atp_proof ctxt fact_names atp_proof = - let val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof in + | used_facts_in_unsound_atp_proof ctxt facts atp_proof = + let val used_facts = used_facts_in_atp_proof ctxt facts atp_proof in if forall (fn (_, (sc, _)) => sc = Global) used_facts andalso - not (is_axiom_used_in_proof (not o null o resolve_conjecture o single) atp_proof) then + not (is_axiom_used_in_proof (is_some o resolve_conjecture) atp_proof) then SOME (map fst used_facts) else NONE @@ -716,16 +708,16 @@ else proof -fun factify_atp_proof fact_names hyp_ts concl_t atp_proof = +fun factify_atp_proof facts hyp_ts concl_t atp_proof = let fun factify_step ((num, ss), _, t, rule, deps) = let val (ss', role', t') = - (case resolve_conjecture ss of + (case resolve_conjectures ss of [j] => if j = length hyp_ts then ([], Conjecture, concl_t) else ([], Hypothesis, nth hyp_ts j) | _ => - (case resolve_fact fact_names ss of + (case resolve_facts facts ss of [] => (ss, Plain, t) | facts => (map fst facts, Axiom, t))) in diff -r b2c629647a14 -r 2b6a96cc64c9 src/HOL/Tools/Metis/metis_generate.ML --- a/src/HOL/Tools/Metis/metis_generate.ML Mon Jun 16 19:40:04 2014 +0200 +++ b/src/HOL/Tools/Metis/metis_generate.ML Mon Jun 16 19:40:59 2014 +0200 @@ -29,11 +29,9 @@ val metis_name_table : ((string * int) * ((type_enc -> string) * bool)) list val reveal_old_skolem_terms : (string * term) list -> term -> term val reveal_lam_lifted : (string * term) list -> term -> term - val prepare_metis_problem : - Proof.context -> type_enc -> string -> thm list -> thm list - -> int Symtab.table * (Metis_Thm.thm * isa_thm) list - * (unit -> (string * int) list) - * ((string * term) list * (string * term) list) + val generate_metis_problem : Proof.context -> type_enc -> string -> thm list -> thm list -> + int Symtab.table * (Metis_Thm.thm * isa_thm) list * (unit -> (string * int) list) + * ((string * term) list * (string * term) list) end structure Metis_Generate : METIS_GENERATE = @@ -172,42 +170,33 @@ else if String.isPrefix conjecture_prefix ident then NONE else if String.isPrefix helper_prefix ident then - case (String.isSuffix typed_helper_suffix ident, - space_explode "_" ident) of + case (String.isSuffix typed_helper_suffix ident, space_explode "_" ident) of (needs_fairly_sound, _ :: const :: j :: _) => - nth (AList.lookup (op =) helper_table (const, needs_fairly_sound) - |> the) - (the (Int.fromString j) - 1) + nth (AList.lookup (op =) helper_table (const, needs_fairly_sound) |> the) + (the (Int.fromString j) - 1) |> snd |> prepare_helper ctxt |> Isa_Raw |> some | _ => raise Fail ("malformed helper identifier " ^ quote ident) else case try (unprefix fact_prefix) ident of SOME s => - let val s = s |> space_explode "_" |> tl |> space_implode "_" - in + let val s = s |> space_explode "_" |> tl |> space_implode "_" in case Int.fromString s of - SOME j => - Meson.make_meta_clause (snd (nth clauses j)) |> Isa_Raw |> some + SOME j => Meson.make_meta_clause (snd (nth clauses j)) |> Isa_Raw |> some | NONE => - if String.isPrefix lam_fact_prefix (unascii_of s) then - Isa_Lambda_Lifted |> some - else - raise Fail ("malformed fact identifier " ^ quote ident) + if String.isPrefix lam_fact_prefix (unascii_of s) then Isa_Lambda_Lifted |> some + else raise Fail ("malformed fact identifier " ^ quote ident) end | NONE => TrueI |> Isa_Raw |> some end | metis_axiom_of_atp _ _ _ _ = raise Fail "not CNF -- expected formula" -fun eliminate_lam_wrappers (Const (@{const_name Metis.lambda}, _) $ t) = - eliminate_lam_wrappers t - | eliminate_lam_wrappers (t $ u) = - eliminate_lam_wrappers t $ eliminate_lam_wrappers u - | eliminate_lam_wrappers (Abs (s, T, t)) = - Abs (s, T, eliminate_lam_wrappers t) +fun eliminate_lam_wrappers (Const (@{const_name Metis.lambda}, _) $ t) = eliminate_lam_wrappers t + | eliminate_lam_wrappers (t $ u) = eliminate_lam_wrappers t $ eliminate_lam_wrappers u + | eliminate_lam_wrappers (Abs (s, T, t)) = Abs (s, T, eliminate_lam_wrappers t) | eliminate_lam_wrappers t = t (* Function to generate metis clauses, including comb and type clauses *) -fun prepare_metis_problem ctxt type_enc lam_trans conj_clauses fact_clauses = +fun generate_metis_problem ctxt type_enc lam_trans conj_clauses fact_clauses = let val (conj_clauses, fact_clauses) = if is_type_enc_polymorphic type_enc then @@ -221,34 +210,31 @@ val num_conjs = length conj_clauses (* Pretend every clause is a "simp" rule, to guide the term ordering. *) val clauses = - map2 (fn j => pair (Int.toString j, (Local, Simp))) - (0 upto num_conjs - 1) conj_clauses @ + map2 (fn j => pair (Int.toString j, (Local, Simp))) (0 upto num_conjs - 1) conj_clauses @ map2 (fn j => pair (Int.toString (num_conjs + j), (Local, Simp))) - (0 upto length fact_clauses - 1) fact_clauses + (0 upto length fact_clauses - 1) fact_clauses val (old_skolems, props) = fold_rev (fn (name, th) => fn (old_skolems, props) => - th |> prop_of |> Logic.strip_imp_concl - |> conceal_old_skolem_terms (length clauses) old_skolems - ||> (lam_trans = liftingN orelse lam_trans = lam_liftingN) - ? eliminate_lam_wrappers - ||> (fn prop => (name, prop) :: props)) - clauses ([], []) + th |> prop_of |> Logic.strip_imp_concl + |> conceal_old_skolem_terms (length clauses) old_skolems + ||> (lam_trans = liftingN orelse lam_trans = lam_liftingN) ? eliminate_lam_wrappers + ||> (fn prop => (name, prop) :: props)) + clauses ([], []) (* val _ = tracing ("PROPS:\n" ^ cat_lines (map (Syntax.string_of_term ctxt o snd) props)) *) val lam_trans = if lam_trans = combsN then no_lamsN else lam_trans - val (atp_problem, _, _, lifted, sym_tab) = - prepare_atp_problem ctxt CNF Hypothesis type_enc Metis lam_trans false - false false [] @{prop False} props + val (atp_problem, _, lifted, sym_tab) = + generate_atp_problem ctxt CNF Hypothesis type_enc Metis lam_trans false false false [] + @{prop False} props (* val _ = tracing ("ATP PROBLEM: " ^ cat_lines (lines_of_atp_problem CNF atp_problem)) *) (* "rev" is for compatibility with existing proof scripts. *) - val axioms = - atp_problem + val axioms = atp_problem |> maps (map_filter (metis_axiom_of_atp ctxt type_enc clauses) o snd) |> rev fun ord_info () = atp_problem_term_order_info atp_problem in (sym_tab, axioms, ord_info, (lifted, old_skolems)) end diff -r b2c629647a14 -r 2b6a96cc64c9 src/HOL/Tools/Metis/metis_tactic.ML --- a/src/HOL/Tools/Metis/metis_tactic.ML Mon Jun 16 19:40:04 2014 +0200 +++ b/src/HOL/Tools/Metis/metis_tactic.ML Mon Jun 16 19:40:59 2014 +0200 @@ -156,8 +156,7 @@ map2 (fn j => fn th => (Thm.get_name_hint th, th |> Drule.eta_contraction_rule - |> Meson_Clausify.cnf_axiom ctxt new_skolem - (lam_trans = combsN) j + |> Meson_Clausify.cnf_axiom ctxt new_skolem (lam_trans = combsN) j ||> map do_lams)) (0 upto length ths0 - 1) ths0 val ths = maps (snd o snd) th_cls_pairs @@ -168,7 +167,7 @@ val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc) val type_enc = type_enc_of_string Strict type_enc val (sym_tab, axioms, ord_info, concealed) = - prepare_metis_problem ctxt type_enc lam_trans cls ths + generate_metis_problem ctxt type_enc lam_trans cls ths fun get_isa_thm mth Isa_Reflexive_or_Trivial = reflexive_or_trivial_of_metis ctxt type_enc sym_tab concealed mth | get_isa_thm mth Isa_Lambda_Lifted = diff -r b2c629647a14 -r 2b6a96cc64c9 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Jun 16 19:40:04 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Jun 16 19:40:59 2014 +0200 @@ -252,7 +252,7 @@ val readable_names = not (Config.get ctxt atp_full_names) val lam_trans = lam_trans |> the_default best_lam_trans val uncurried_aliases = uncurried_aliases |> the_default best_uncurried_aliases - val value as (atp_problem, _, fact_names, _, _) = + val value as (atp_problem, _, _, _) = if cache_key = SOME key then cache_value else @@ -261,8 +261,8 @@ |> take num_facts |> not (is_type_enc_polymorphic type_enc) ? monomorphize_facts |> map (apsnd prop_of) - |> prepare_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 format prem_role type_enc atp_mode lam_trans + uncurried_aliases readable_names true hyp_ts concl_t fun sel_weights () = atp_problem_selection_weights atp_problem fun ord_info () = atp_problem_term_order_info atp_problem @@ -275,11 +275,13 @@ val command = "(exec 2>&1; " ^ File.shell_path command0 ^ " " ^ args ^ " " ^ ")" |> enclose "TIMEFORMAT='%3R'; { time " " ; }" + val _ = atp_problem |> lines_of_atp_problem format ord ord_info |> cons ("% " ^ command ^ "\n" ^ (if comment = "" then "" else "% " ^ comment ^ "\n")) |> File.write_list prob_path + val ((output, run_time), (atp_proof, outcome)) = TimeLimit.timeLimit generous_slice_timeout Isabelle_System.bash_output command |>> (if overlord then prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") else I) @@ -290,10 +292,11 @@ |>> atp_proof_of_tstplike_proof (perhaps (try (unprefix remote_prefix)) name) atp_problem handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofIncomplete))) handle TimeLimit.TimeOut => (("", slice_timeout), ([], SOME TimedOut)) + val outcome = (case outcome of NONE => - (case used_facts_in_unsound_atp_proof ctxt fact_names atp_proof + (case used_facts_in_unsound_atp_proof ctxt (map fst facts) atp_proof |> Option.map (sort string_ord) of SOME facts => let val failure = UnsoundProof (is_type_enc_sound type_enc, facts) in @@ -321,7 +324,7 @@ end | maybe_run_slice _ result = result in - ((NONE, ([], Symtab.empty, Vector.fromList [], [], Symtab.empty)), + ((NONE, ([], Symtab.empty, [], Symtab.empty)), ("", Time.zeroTime, [], [], SOME InternalError), NONE) |> fold maybe_run_slice actual_slices end @@ -333,8 +336,8 @@ if dest_dir = "" then () else File.write (Path.explode (Path.implode prob_path ^ "_proof")) output - val ((_, (_, pool, fact_names, lifted, sym_tab)), - (output, run_time, used_from, atp_proof, outcome), SOME (format, type_enc)) = + val ((_, (_, pool, lifted, sym_tab)), (output, run_time, used_from, atp_proof, outcome), + SOME (format, type_enc)) = with_cleanup clean_up run () |> tap export val important_message = @@ -347,7 +350,7 @@ (case outcome of NONE => let - val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof + val used_facts = used_facts_in_atp_proof ctxt (map fst used_from) atp_proof val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof val meths = bunch_of_proof_methods (smt_proofs <> SOME false) needs_full_types @@ -362,6 +365,7 @@ fn preplay => let val _ = if verbose then Output.urgent_message "Generating proof text..." else () + fun isar_params () = let val metis_type_enc = @@ -372,11 +376,12 @@ atp_proof |> termify_atp_proof ctxt name format type_enc pool lifted sym_tab |> introduce_spass_skolem - |> factify_atp_proof fact_names hyp_ts concl_t + |> factify_atp_proof (map fst used_from) hyp_ts concl_t in (verbose, (metis_type_enc, metis_lam_trans), preplay_timeout, compress, try0, minimize <> SOME false, atp_proof, goal) end + val one_line_params = (preplay, proof_banner mode name, used_facts, choose_minimize_command thy params minimize_command name preplay, subgoal,