111 let |
111 let |
112 val {context = ctxt, facts = chained_ths, goal} = Proof.goal pre |
112 val {context = ctxt, facts = chained_ths, goal} = Proof.goal pre |
113 val prover = AList.lookup (op =) args "prover" |> the_default default_prover |
113 val prover = AList.lookup (op =) args "prover" |> the_default default_prover |
114 val params as {max_facts, ...} = |
114 val params as {max_facts, ...} = |
115 Sledgehammer_Commands.default_params ctxt args |
115 Sledgehammer_Commands.default_params ctxt args |
116 val default_max_facts = Sledgehammer_Provers.default_max_facts_of_prover ctxt prover |
116 val default_max_facts = Sledgehammer_Prover.default_max_facts_of_prover ctxt prover |
117 val is_appropriate_prop = |
117 val is_appropriate_prop = |
118 Sledgehammer_Provers.is_appropriate_prop_of_prover ctxt default_prover |
118 Sledgehammer_Prover.is_appropriate_prop_of_prover ctxt default_prover |
119 val relevance_fudge = |
119 val relevance_fudge = |
120 extract_relevance_fudge args Sledgehammer_MePo.default_relevance_fudge |
120 extract_relevance_fudge args Sledgehammer_MePo.default_relevance_fudge |
121 val subgoal = 1 |
121 val subgoal = 1 |
122 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal subgoal ctxt |
122 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal subgoal ctxt |
123 val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover |
123 val ho_atp = Sledgehammer_Prover.is_ho_atp ctxt prover |
124 val reserved = Sledgehammer_Util.reserved_isar_keyword_table () |
124 val reserved = Sledgehammer_Util.reserved_isar_keyword_table () |
125 val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt |
125 val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt |
126 val facts = |
126 val facts = |
127 Sledgehammer_Fact.nearly_all_facts ctxt ho_atp |
127 Sledgehammer_Fact.nearly_all_facts ctxt ho_atp |
128 Sledgehammer_Fact.no_fact_override reserved css_table chained_ths |
128 Sledgehammer_Fact.no_fact_override reserved css_table chained_ths |