# HG changeset patch # User blanchet # Date 1369723961 -7200 # Node ID 2281f33e8da60508b7a08b6a78096239370ed528 # Parent 056ec8201667933b7d6aa598051ee90f31c45c20 redid rac7830871177 to avoid duplicate fixed variable (e.g. lemma "P (a::nat)" proof - have "!!a::int. Q a" sledgehammer [e]) diff -r 056ec8201667 -r 2281f33e8da6 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue May 28 08:36:12 2013 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue May 28 08:52:41 2013 +0200 @@ -454,7 +454,7 @@ Sledgehammer_Provers.default_max_facts_of_prover ctxt slice prover_name val is_appropriate_prop = Sledgehammer_Provers.is_appropriate_prop_of_prover ctxt prover_name - val ((_, hyp_ts, concl_t), _) = ATP_Util.strip_subgoal goal i ctxt + val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal i ctxt val time_limit = (case hard_timeout of NONE => I diff -r 056ec8201667 -r 2281f33e8da6 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Tue May 28 08:36:12 2013 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Tue May 28 08:52:41 2013 +0200 @@ -124,8 +124,7 @@ extract_relevance_fudge args (Sledgehammer_Provers.relevance_fudge_of_prover ctxt prover) val subgoal = 1 - val ((_, hyp_ts, concl_t), ctxt) = - ATP_Util.strip_subgoal goal subgoal ctxt + val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal subgoal ctxt val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover val reserved = Sledgehammer_Util.reserved_isar_keyword_table () val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt diff -r 056ec8201667 -r 2281f33e8da6 src/HOL/TPTP/mash_eval.ML --- a/src/HOL/TPTP/mash_eval.ML Tue May 28 08:36:12 2013 +0200 +++ b/src/HOL/TPTP/mash_eval.ML Tue May 28 08:52:41 2013 +0200 @@ -109,7 +109,7 @@ SOME (_, th) => th | NONE => error ("No fact called \"" ^ name ^ "\".") val goal = goal_of_thm (Proof_Context.theory_of ctxt) th - val ((_, hyp_ts, concl_t), _) = ATP_Util.strip_subgoal goal 1 ctxt + val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal 1 ctxt val isar_deps = isar_dependencies_of name_tabs th val facts = facts diff -r 056ec8201667 -r 2281f33e8da6 src/HOL/TPTP/mash_export.ML --- a/src/HOL/TPTP/mash_export.ML Tue May 28 08:36:12 2013 +0200 +++ b/src/HOL/TPTP/mash_export.ML Tue May 28 08:52:41 2013 +0200 @@ -207,7 +207,7 @@ val name = nickname_of_thm th val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name) val goal = goal_of_thm (Proof_Context.theory_of ctxt) th - val ((_, hyp_ts, concl_t), _) = ATP_Util.strip_subgoal goal 1 ctxt + val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal 1 ctxt val isar_deps = isar_dependencies_of name_tabs th in if is_bad_query ctxt ho_atp step j th isar_deps then diff -r 056ec8201667 -r 2281f33e8da6 src/HOL/TPTP/sledgehammer_tactics.ML --- a/src/HOL/TPTP/sledgehammer_tactics.ML Tue May 28 08:36:12 2013 +0200 +++ b/src/HOL/TPTP/sledgehammer_tactics.ML Tue May 28 08:52:41 2013 +0200 @@ -32,7 +32,7 @@ val name = hd provers val prover = get_prover ctxt mode name val default_max_facts = default_max_facts_of_prover ctxt slice name - val ((_, hyp_ts, concl_t), _) = ATP_Util.strip_subgoal goal i ctxt + val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal i ctxt val ho_atp = exists (is_ho_atp ctxt) provers val reserved = reserved_isar_keyword_table () val css_table = clasimpset_rule_table_of ctxt diff -r 056ec8201667 -r 2281f33e8da6 src/HOL/Tools/ATP/atp_util.ML --- a/src/HOL/Tools/ATP/atp_util.ML Tue May 28 08:36:12 2013 +0200 +++ b/src/HOL/Tools/ATP/atp_util.ML Tue May 28 08:52:41 2013 +0200 @@ -49,8 +49,7 @@ val transform_elim_prop : term -> term val specialize_type : theory -> (string * typ) -> term -> term val strip_subgoal : - thm -> int -> Proof.context - -> ((string * typ) list * term list * term) * Proof.context + thm -> int -> Proof.context -> (string * typ) list * term list * term end; structure ATP_Util : ATP_UTIL = @@ -432,17 +431,11 @@ fun strip_subgoal goal i ctxt = let - val (t, ((frees, params), ctxt)) = + val (t, (frees, params)) = Logic.goal_params (prop_of goal) i - ||> map dest_Free - ||> map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) - ||> (fn fixes => - ctxt |> Variable.set_body false - |> Proof_Context.add_fixes fixes - |>> map2 (fn (_, SOME T, _) => fn s => (s, T)) fixes) - ||> apfst (`(map Free)) + ||> (map dest_Free #> Variable.variant_frees ctxt [] #> `(map Free)) val hyp_ts = t |> Logic.strip_assums_hyp |> map (curry subst_bounds frees) val concl_t = t |> Logic.strip_assums_concl |> curry subst_bounds frees - in ((rev params, hyp_ts, concl_t), ctxt) end + in (rev params, hyp_ts, concl_t) end end; diff -r 056ec8201667 -r 2281f33e8da6 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Tue May 28 08:36:12 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Tue May 28 08:52:41 2013 +0200 @@ -707,7 +707,7 @@ let val thy = Proof_Context.theory_of ctxt val goal = goal_of_thm thy th - val ((_, hyp_ts, concl_t), _) = ATP_Util.strip_subgoal goal 1 ctxt + val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal 1 ctxt val facts = facts |> filter (fn (_, th') => thm_less (th', th)) fun nickify ((_, stature), th) = ((nickname_of_thm th, stature), th) fun is_dep dep (_, th) = nickname_of_thm th = dep diff -r 056ec8201667 -r 2281f33e8da6 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue May 28 08:36:12 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue May 28 08:52:41 2013 +0200 @@ -686,7 +686,7 @@ val atp_mode = if Config.get ctxt completish then Sledgehammer_Completish else Sledgehammer - val ((_, hyp_ts, concl_t), ctxt') = strip_subgoal goal subgoal ctxt + val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt val (dest_dir, problem_prefix) = if overlord then overlord_file_location_of_prover name else (Config.get ctxt dest_dir, Config.get ctxt problem_prefix) diff -r 056ec8201667 -r 2281f33e8da6 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Tue May 28 08:36:12 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Tue May 28 08:52:41 2013 +0200 @@ -649,7 +649,13 @@ fact_names, lifted, sym_tab, atp_proof, goal) (one_line_params as (_, _, _, _, subgoal, subgoal_count)) = let - val ((params, hyp_ts, concl_t), ctxt) = strip_subgoal goal subgoal ctxt + val (params, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt + val (_, ctxt) = + params + |> map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) + |> (fn fixes => + ctxt |> Variable.set_body false + |> Proof_Context.add_fixes fixes) val one_line_proof = one_line_proof_text 0 one_line_params val type_enc = if is_typed_helper_used_in_atp_proof atp_proof then full_typesN diff -r 056ec8201667 -r 2281f33e8da6 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue May 28 08:36:12 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue May 28 08:52:41 2013 +0200 @@ -198,7 +198,7 @@ state |> Proof.map_context (Config.put SMT_Config.verbose debug) val ctxt = Proof.context_of state val {facts = chained, goal, ...} = Proof.goal state - val ((_, hyp_ts, concl_t), _) = strip_subgoal goal i ctxt + val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt val ho_atp = exists (is_ho_atp ctxt) provers val reserved = reserved_isar_keyword_table () val css = clasimpset_rule_table_of ctxt