# HG changeset patch # User blanchet # Date 1306224063 -7200 # Node ID 74415622d2933549c5bf9bc78d03d4f4b4d1e3d4 # Parent 13cb8895f53815b2a8a8a4830162561de8d44e27 more work on parsing LEO-II proofs and extracting uses of extensionality diff -r 13cb8895f538 -r 74415622d293 src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Tue May 24 10:01:00 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_problem.ML Tue May 24 10:01:03 2011 +0200 @@ -25,17 +25,31 @@ * string fo_term option * string fo_term option type 'a problem = (string * 'a problem_line list) list - (* official TPTP syntax *) + val tptp_cnf : string + val tptp_fof : string + val tptp_tff : string + val tptp_thf : string val tptp_special_prefix : string val tptp_has_type : string val tptp_type_of_types : string val tptp_bool_type : string val tptp_individual_type : string val tptp_fun_type : string + val tptp_prod_type : string + val tptp_forall : string + val tptp_exists : string + val tptp_not : string + val tptp_and : string + val tptp_or : string + val tptp_implies : string + val tptp_if : string + val tptp_iff : string + val tptp_not_iff : string + val tptp_app : string + val tptp_not_infix : string + val tptp_equal : string val tptp_false : string val tptp_true : string - val tptp_not : string - val tptp_app : string val is_atp_variable : string -> bool val mk_anot : ('a, 'b, 'c) formula -> ('a, 'b, 'c) formula val mk_aconn : @@ -78,16 +92,31 @@ type 'a problem = (string * 'a problem_line list) list (* official TPTP syntax *) +val tptp_cnf = "cnf" +val tptp_fof = "fof" +val tptp_tff = "tff" +val tptp_thf = "thf" val tptp_special_prefix = "$" val tptp_has_type = ":" val tptp_type_of_types = "$tType" val tptp_bool_type = "$o" val tptp_individual_type = "$i" val tptp_fun_type = ">" +val tptp_prod_type = "*" +val tptp_forall = "!" +val tptp_exists = "?" +val tptp_not = "~" +val tptp_and = "&" +val tptp_or = "|" +val tptp_implies = "=>" +val tptp_if = "<=" +val tptp_iff = "<=>" +val tptp_not_iff = "<~>" +val tptp_app = "@" +val tptp_not_infix = "!" +val tptp_equal = "=" val tptp_false = "$false" val tptp_true = "$true" -val tptp_not = "~" -val tptp_app = "@" fun is_atp_variable s = Char.isUpper (String.sub (s, 0)) @@ -130,36 +159,39 @@ (case strip_tff_type ty of ([], s) => s | ([s'], s) => s' ^ " " ^ tptp_fun_type ^ " " ^ s - | (ss, s) => "(" ^ space_implode " * " ss ^ ") " ^ tptp_fun_type ^ " " ^ s) + | (ss, s) => + "(" ^ space_implode tptp_prod_type ss ^ ") " ^ tptp_fun_type ^ " " ^ s) | string_for_type _ _ = raise Fail "unexpected type in untyped format" fun string_for_term _ (ATerm (s, [])) = s | string_for_term format (ATerm ("equal", ts)) = - space_implode " = " (map (string_for_term format) ts) + space_implode (" " ^ tptp_equal ^ " ") (map (string_for_term format) ts) |> format = THF ? enclose "(" ")" | string_for_term format (ATerm ("[]", ts)) = (* used for lists in the optional "source" field of a derivation *) "[" ^ commas (map (string_for_term format) ts) ^ "]" | string_for_term format (ATerm (s, ts)) = let val ss = map (string_for_term format) ts in - if format = THF then "(" ^ space_implode " @ " (s :: ss) ^ ")" - else s ^ "(" ^ commas ss ^ ")" + if format = THF then + "(" ^ space_implode (" " ^ tptp_app ^ " ") (s :: ss) ^ ")" + else + s ^ "(" ^ commas ss ^ ")" end -fun string_for_quantifier AForall = "!" - | string_for_quantifier AExists = "?" +fun string_for_quantifier AForall = tptp_forall + | string_for_quantifier AExists = tptp_exists fun string_for_connective ANot = tptp_not - | string_for_connective AAnd = "&" - | string_for_connective AOr = "|" - | string_for_connective AImplies = "=>" - | string_for_connective AIf = "<=" - | string_for_connective AIff = "<=>" - | string_for_connective ANotIff = "<~>" + | string_for_connective AAnd = tptp_and + | string_for_connective AOr = tptp_or + | string_for_connective AImplies = tptp_implies + | string_for_connective AIf = tptp_if + | string_for_connective AIff = tptp_iff + | string_for_connective ANotIff = tptp_not_iff fun string_for_bound_var format (s, ty) = s ^ (if format = TFF orelse format = THF then - " : " ^ + " " ^ tptp_has_type ^ " " ^ string_for_type format (ty |> the_default (AType tptp_individual_type)) else "") @@ -169,7 +201,8 @@ "[" ^ commas (map (string_for_bound_var format) xs) ^ "] : " ^ string_for_formula format phi ^ ")" | string_for_formula format (AConn (ANot, [AAtom (ATerm ("equal", ts))])) = - space_implode " != " (map (string_for_term format) ts) + space_implode (" " ^ tptp_not_infix ^ tptp_equal ^ " ") + (map (string_for_term format) ts) |> format = THF ? enclose "(" ")" | string_for_formula format (AConn (c, [phi])) = "(" ^ string_for_connective c ^ " " ^ string_for_formula format phi ^ ")" @@ -181,10 +214,10 @@ val default_source = ATerm ("inference", ATerm ("isabelle", []) :: replicate 2 (ATerm ("[]", []))) -fun string_for_format CNF_UEQ = "cnf" - | string_for_format FOF = "fof" - | string_for_format TFF = "tff" - | string_for_format THF = "thf" +fun string_for_format CNF_UEQ = tptp_cnf + | string_for_format FOF = tptp_fof + | string_for_format TFF = tptp_tff + | string_for_format THF = tptp_thf fun string_for_problem_line format (Decl (ident, sym, ty)) = string_for_format format ^ "(" ^ ident ^ ", type,\n " ^ sym ^ " : " ^ diff -r 13cb8895f538 -r 74415622d293 src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Tue May 24 10:01:00 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_proof.ML Tue May 24 10:01:03 2011 +0200 @@ -53,11 +53,12 @@ val extract_tstplike_proof_and_outcome : bool -> bool -> int -> (string * string) list -> (failure * string) list -> string -> string * failure option - val is_same_step : step_name * step_name -> bool + val is_same_atp_step : step_name -> step_name -> bool val scan_general_id : string list -> string * string list val parse_formula : string list -> (string, 'a, string fo_term) formula * string list val atp_proof_from_tstplike_proof : string problem -> string -> string proof + val clean_up_atp_proof_dependencies : string proof -> string proof val map_term_names_in_atp_proof : (string -> string) -> string proof -> string proof val nasty_atp_proof : string Symtab.table -> string proof -> string proof @@ -142,10 +143,8 @@ fun involving [] = "" | involving ss = "involving " ^ commas_quote ss ^ " " -fun string_for_failure Unprovable = - "The problem is unprovable." - | string_for_failure IncompleteUnprovable = - "The prover gave up." +fun string_for_failure Unprovable = "The problem is unprovable." + | string_for_failure IncompleteUnprovable = "The prover gave up." | string_for_failure ProofMissing = "The prover claims the conjecture is a theorem but did not provide a proof." | string_for_failure ProofIncomplete = @@ -239,14 +238,17 @@ type step_name = string * string option -fun is_same_step p = p |> pairself fst |> op = +fun is_same_atp_step (s1, _) (s2, _) = s1 = s2 + +val vampire_fact_prefix = "f" fun step_name_ord p = let val q = pairself fst p in (* The "unprefix" part is to cope with remote Vampire's output. The proper solution would be to perform a topological sort, e.g. using the nice "Graph" functor. *) - case pairself (Int.fromString o perhaps (try (unprefix "f"))) q of + case pairself (Int.fromString + o perhaps (try (unprefix vampire_fact_prefix))) q of (NONE, NONE) => string_ord q | (NONE, SOME _) => LESS | (SOME _, NONE) => GREATER @@ -282,23 +284,32 @@ >> flat) x fun list_app (f, args) = - fold (fn arg => fn f => ATerm (tptp_app_op, [f, arg])) args f + fold (fn arg => fn f => ATerm (tptp_app, [f, arg])) args f -fun parse_arg x = - (scan_general_id - (* We ignore TFF and THF types for now. *) - --| Scan.repeat (($$ ":" || $$ ">") |-- parse_arg) - -- Scan.optional ($$ "(" |-- parse_terms --| $$ ")") [] - >> ATerm) x +(* We ignore TFF and THF types for now. *) +fun parse_type_stuff x = + Scan.repeat (($$ tptp_has_type || $$ tptp_fun_type) |-- parse_arg) x +and parse_arg x = + ($$ "(" |-- parse_term --| $$ ")" --| parse_type_stuff + || scan_general_id --| parse_type_stuff + -- Scan.optional ($$ "(" |-- parse_terms --| $$ ")") [] + >> ATerm) x and parse_app x = - (parse_arg -- Scan.repeat ($$ tptp_app_op |-- parse_arg) >> list_app) x + (parse_arg -- Scan.repeat ($$ tptp_app |-- parse_arg) >> list_app) x and parse_term x = - (parse_app -- Scan.optional) + (parse_app -- Scan.option (Scan.option ($$ tptp_not_infix) --| $$ tptp_equal + -- parse_app) + >> (fn (u1, NONE) => u1 + | (u1, SOME (NONE, u2)) => ATerm ("equal", [u1, u2]) + | (u1, SOME (SOME _, u2)) => + ATerm (tptp_not, [ATerm ("equal", [u1, u2])]))) x and parse_terms x = (parse_term ::: Scan.repeat ($$ "," |-- parse_term)) x +(* TODO: Avoid duplication with "parse_term" above. *) fun parse_atom x = - (parse_term -- Scan.option (Scan.option ($$ "!") --| $$ "=" -- parse_term) + (parse_term -- Scan.option (Scan.option ($$ tptp_not_infix) --| $$ tptp_equal + -- parse_term) >> (fn (u1, NONE) => AAtom u1 | (u1, SOME (NONE, u2)) => AAtom (ATerm ("equal", [u1, u2])) | (u1, SOME (SOME _, u2)) => @@ -309,29 +320,42 @@ (* TPTP formulas are fully parenthesized, so we don't need to worry about operator precedence. *) fun parse_literal x = - ((Scan.repeat ($$ "~") >> length) + ((Scan.repeat ($$ tptp_not) >> length) -- ($$ "(" |-- parse_formula --| $$ ")" || parse_quantified_formula || parse_atom) >> (fn (n, phi) => phi |> n mod 2 = 1 ? mk_anot)) x and parse_formula x = (parse_literal - -- Scan.option ((Scan.this_string "=>" >> K AImplies - || Scan.this_string "<=>" >> K AIff - || Scan.this_string "<~>" >> K ANotIff - || Scan.this_string "<=" >> K AIf - || $$ "|" >> K AOr - || $$ "&" >> K AAnd) + -- Scan.option ((Scan.this_string tptp_implies >> K AImplies + || Scan.this_string tptp_iff >> K AIff + || Scan.this_string tptp_not_iff >> K ANotIff + || Scan.this_string tptp_if >> K AIf + || $$ tptp_or >> K AOr + || $$ tptp_and >> K AAnd) -- parse_formula) >> (fn (phi1, NONE) => phi1 | (phi1, SOME (c, phi2)) => mk_aconn c phi1 phi2)) x and parse_quantified_formula x = - (($$ "!" >> K AForall || $$ "?" >> K AExists) + (($$ tptp_forall >> K AForall || $$ tptp_exists >> K AExists) --| $$ "[" -- parse_terms --| $$ "]" --| $$ ":" -- parse_literal >> (fn ((q, ts), phi) => (* We ignore TFF and THF types for now. *) AQuant (q, map (rpair NONE o fo_term_head) ts, phi))) x +fun skip_formula ss = + let + fun skip _ [] = [] + | skip 0 (ss as "," :: _) = ss + | skip 0 (ss as ")" :: _) = ss + | skip 0 (ss as "]" :: _) = ss + | skip n ("(" :: ss) = skip (n + 1) ss + | skip n ("[" :: ss) = skip (n + 1) ss + | skip n ("]" :: ss) = skip (n - 1) ss + | skip n (")" :: ss) = skip (n - 1) ss + | skip n (_ :: ss) = skip n ss + in (AAtom (ATerm ("", [])), skip 0 ss) end + val parse_tstp_extra_arguments = Scan.optional ($$ "," |-- parse_annotation --| Scan.option ($$ "," |-- parse_annotations)) [] @@ -384,10 +408,11 @@ \). The could be an identifier, but we assume integers. *) fun parse_tstp_line problem = - ((Scan.this_string "cnf" || Scan.this_string "fof" || Scan.this_string "tff" - || Scan.this_string "thf") -- $$ "(") + ((Scan.this_string tptp_cnf || Scan.this_string tptp_fof + || Scan.this_string tptp_tff || Scan.this_string tptp_thf) -- $$ "(") |-- scan_general_id --| $$ "," -- Symbol.scan_id --| $$ "," - -- parse_formula -- parse_tstp_extra_arguments --| $$ ")" --| $$ "." + -- (parse_formula || skip_formula) -- parse_tstp_extra_arguments --| $$ ")" + --| $$ "." >> (fn (((num, role), phi), deps) => let val (name, deps) = @@ -413,7 +438,7 @@ | AAtom (ATerm ("equal", _)) => (* Vampire's equality proxy axiom *) Inference (name, phi, map (rpair NONE) deps) - | _ => raise Fail "malformed definition") + | _ => raise UNRECOGNIZED_ATP_PROOF ()) | _ => Inference (name, phi, map (rpair NONE) deps) end) @@ -462,20 +487,22 @@ (Scan.repeat1 (parse_line problem)))) |> fst -fun clean_up_dependency seen dep = find_first (curry is_same_step dep) seen -fun clean_up_dependencies _ [] = [] - | clean_up_dependencies seen ((step as Definition (name, _, _)) :: steps) = - step :: clean_up_dependencies (name :: seen) steps - | clean_up_dependencies seen (Inference (name, u, deps) :: steps) = - Inference (name, u, map_filter (clean_up_dependency seen) deps) :: - clean_up_dependencies (name :: seen) steps - fun atp_proof_from_tstplike_proof _ "" = [] | atp_proof_from_tstplike_proof problem s = s ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *) |> parse_proof problem |> sort (step_name_ord o pairself step_name) - |> clean_up_dependencies [] + +fun clean_up_dependencies _ [] = [] + | clean_up_dependencies seen ((step as Definition (name, _, _)) :: steps) = + step :: clean_up_dependencies (name :: seen) steps + | clean_up_dependencies seen (Inference (name, u, deps) :: steps) = + Inference (name, u, + map_filter (fn dep => find_first (is_same_atp_step dep) seen) + deps) :: + clean_up_dependencies (name :: seen) steps + +val clean_up_atp_proof_dependencies = clean_up_dependencies [] fun map_term_names_in_term f (ATerm (s, ts)) = ATerm (f s, map (map_term_names_in_term f) ts) diff -r 13cb8895f538 -r 74415622d293 src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Tue May 24 10:01:00 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Tue May 24 10:01:03 2011 +0200 @@ -16,8 +16,7 @@ string * minimize_command * type_system * string proof * int * (string * locality) list vector * int list * thm * int type isar_params = - Proof.context * bool * int * string Symtab.table * int list list - * int Symtab.table + bool * int * string Symtab.table * int list list * int Symtab.table type text_result = string * (string * locality) list val repair_conjecture_shape_and_fact_names : @@ -25,11 +24,11 @@ -> (string * locality) list vector -> int list -> int list list * int * (string * locality) list vector * int list val used_facts_in_atp_proof : - type_system -> int -> (string * locality) list vector -> string proof - -> (string * locality) list + Proof.context -> type_system -> int -> (string * locality) list vector + -> string proof -> (string * locality) list val used_facts_in_unsound_atp_proof : - type_system -> int list list -> int -> (string * locality) list vector - -> string proof -> string list option + Proof.context -> type_system -> int list list -> int + -> (string * locality) list vector -> string proof -> string list option val apply_on_subgoal : string -> int -> int -> string val command_call : string -> string list -> string val try_command_line : string -> string -> string @@ -37,9 +36,11 @@ val split_used_facts : (string * locality) list -> (string * locality) list * (string * locality) list - val metis_proof_text : metis_params -> text_result - val isar_proof_text : isar_params -> metis_params -> text_result - val proof_text : bool -> isar_params -> metis_params -> text_result + val metis_proof_text : Proof.context -> metis_params -> text_result + val isar_proof_text : + Proof.context -> isar_params -> metis_params -> text_result + val proof_text : + Proof.context -> bool -> isar_params -> metis_params -> text_result end; structure Sledgehammer_ATP_Reconstruct : SLEDGEHAMMER_ATP_RECONSTRUCT = @@ -57,8 +58,7 @@ string * minimize_command * type_system * string proof * int * (string * locality) list vector * int list * thm * int type isar_params = - Proof.context * bool * int * string Symtab.table * int list list - * int Symtab.table + bool * int * string Symtab.table * int list list * int Symtab.table type text_result = string * (string * locality) list fun is_head_digit s = Char.isDigit (String.sub (s, 0)) @@ -182,23 +182,39 @@ SOME i => member (op =) typed_helpers i | NONE => false) -fun add_fact type_sys facts_offset fact_names (Inference (name, _, [])) = - union (op =) (resolve_fact type_sys facts_offset fact_names name) - | add_fact _ _ _ _ = I +val leo2_ext = "extcnf_equal_neg" +val isa_ext = Thm.get_name_hint @{thm ext} +val isa_short_ext = Long_Name.base_name isa_ext + +fun ext_name ctxt = + if Thm.eq_thm_prop (@{thm ext}, + singleton (Attrib.eval_thms ctxt) (Facts.named isa_short_ext, [])) then + isa_short_ext + else + isa_ext -fun used_facts_in_atp_proof type_sys facts_offset fact_names atp_proof = +fun add_fact _ type_sys facts_offset fact_names (Inference (name, _, [])) = + union (op =) (resolve_fact type_sys facts_offset fact_names name) + | add_fact ctxt _ _ _ (Inference (_, _, deps)) = + if AList.defined (op =) deps leo2_ext then + insert (op =) (ext_name ctxt, General (* or Chained... *)) + else + I + | add_fact _ _ _ _ _ = I + +fun used_facts_in_atp_proof ctxt type_sys facts_offset fact_names atp_proof = if null atp_proof then Vector.foldl (op @) [] fact_names - else fold (add_fact type_sys facts_offset fact_names) atp_proof [] + else fold (add_fact ctxt type_sys facts_offset fact_names) atp_proof [] fun is_conjecture_referred_to_in_proof conjecture_shape = exists (fn Inference (name, _, []) => is_conjecture conjecture_shape name | _ => false) -fun used_facts_in_unsound_atp_proof type_sys conjecture_shape facts_offset +fun used_facts_in_unsound_atp_proof ctxt type_sys conjecture_shape facts_offset fact_names atp_proof = let - val used_facts = used_facts_in_atp_proof type_sys facts_offset fact_names - atp_proof + val used_facts = + used_facts_in_atp_proof ctxt type_sys facts_offset fact_names atp_proof in if forall (is_locality_global o snd) used_facts andalso not (is_conjecture_referred_to_in_proof conjecture_shape atp_proof) then @@ -244,11 +260,11 @@ exists (fn Inference (name, _, []) => is_typed_helper typed_helpers name | _ => false) -fun metis_proof_text (banner, minimize_command, type_sys, atp_proof, - facts_offset, fact_names, typed_helpers, goal, i) = +fun metis_proof_text ctxt (banner, minimize_command, type_sys, atp_proof, + facts_offset, fact_names, typed_helpers, goal, i) = let val (chained, extra) = - atp_proof |> used_facts_in_atp_proof type_sys facts_offset fact_names + atp_proof |> used_facts_in_atp_proof ctxt type_sys facts_offset fact_names |> split_used_facts val full_types = uses_typed_helpers typed_helpers atp_proof val n = Logic.count_prems (prop_of goal) @@ -561,7 +577,7 @@ val is_only_type_information = curry (op aconv) HOLogic.true_const fun replace_one_dependency (old, new) dep = - if is_same_step (dep, old) then new else [dep] + if is_same_atp_step dep old then new else [dep] fun replace_dependencies_in_line _ (line as Definition _) = line | replace_dependencies_in_line p (Inference (name, t, deps)) = Inference (name, t, fold (union (op =) o replace_one_dependency p) deps []) @@ -692,6 +708,7 @@ let val lines = atp_proof + |> clean_up_atp_proof_dependencies |> nasty_atp_proof pool |> map_term_names_in_atp_proof repair_name |> decode_lines ctxt sym_tab tfrees @@ -995,17 +1012,17 @@ (if n <> 1 then "next" else "qed") in do_proof end -fun isar_proof_text (ctxt, debug, isar_shrink_factor, pool, conjecture_shape, - sym_tab) - (metis_params as (_, _, type_sys, atp_proof, facts_offset, - fact_names, typed_helpers, goal, i)) = +fun isar_proof_text ctxt + (debug, isar_shrink_factor, pool, conjecture_shape, sym_tab) + (metis_params as (_, _, type_sys, atp_proof, facts_offset, fact_names, + typed_helpers, goal, i)) = let val (params, hyp_ts, concl_t) = strip_subgoal goal i val frees = fold Term.add_frees (concl_t :: hyp_ts) [] val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) [] val full_types = uses_typed_helpers typed_helpers atp_proof val n = Logic.count_prems (prop_of goal) - val (one_line_proof, lemma_names) = metis_proof_text metis_params + val (one_line_proof, lemma_names) = metis_proof_text ctxt metis_params fun isar_proof_for () = case isar_proof_from_atp_proof pool ctxt type_sys tfrees isar_shrink_factor atp_proof conjecture_shape facts_offset @@ -1026,8 +1043,7 @@ |> the_default "\nWarning: The Isar proof construction failed." in (one_line_proof ^ isar_proof, lemma_names) end -fun proof_text isar_proof isar_params metis_params = - (if isar_proof then isar_proof_text isar_params else metis_proof_text) - metis_params +fun proof_text ctxt isar_proof isar_params = + if isar_proof then isar_proof_text ctxt isar_params else metis_proof_text ctxt end; diff -r 13cb8895f538 -r 74415622d293 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue May 24 10:01:00 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue May 24 10:01:03 2011 +0200 @@ -622,7 +622,7 @@ val outcome = case outcome of NONE => - used_facts_in_unsound_atp_proof type_sys + used_facts_in_unsound_atp_proof ctxt type_sys conjecture_shape facts_offset fact_names atp_proof |> Option.map (fn facts => UnsoundProof (is_type_sys_virtually_sound type_sys, @@ -656,8 +656,8 @@ (result as ((_, _, facts_offset, fact_names, _, _), (_, _, type_sys, atp_proof, SOME (UnsoundProof (false, _))))) = - (case used_facts_in_atp_proof type_sys facts_offset fact_names - atp_proof of + (case used_facts_in_atp_proof ctxt type_sys facts_offset + fact_names atp_proof of [] => result | new_baddies => if slicing andalso iter < atp_blacklist_max_iters - 1 then @@ -712,18 +712,18 @@ else "") val isar_params = - (ctxt, debug, isar_shrink_factor, pool, conjecture_shape, sym_tab) + (debug, isar_shrink_factor, pool, conjecture_shape, sym_tab) val metis_params = (proof_banner auto, minimize_command, type_sys, atp_proof, facts_offset, fact_names, typed_helpers, goal, subgoal) val (outcome, (message, used_facts)) = case outcome of NONE => - (NONE, proof_text isar_proof isar_params metis_params + (NONE, proof_text ctxt isar_proof isar_params metis_params |>> append_to_message) | SOME failure => if failure = ProofMissing orelse failure = ProofIncomplete then - (NONE, metis_proof_text metis_params |>> append_to_message) + (NONE, metis_proof_text ctxt metis_params |>> append_to_message) else (outcome, (string_for_failure failure, [])) in diff -r 13cb8895f538 -r 74415622d293 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue May 24 10:01:00 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue May 24 10:01:03 2011 +0200 @@ -44,7 +44,7 @@ val auto_minimize_min_facts = Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts} - (fn generic => (* ### Config.get_generic generic binary_min_facts *) 10000 (*###*)) + (fn generic => Config.get_generic generic binary_min_facts) fun get_minimizing_prover ctxt auto name (params as {debug, verbose, explicit_apply, ...}) minimize_command