equal
deleted
inserted
replaced
26 |
26 |
27 val max_facts_slack = 2 |
27 val max_facts_slack = 2 |
28 |
28 |
29 val all_names = |
29 val all_names = |
30 filter_out is_likely_tautology_or_too_meta |
30 filter_out is_likely_tautology_or_too_meta |
31 #> map (rpair () o Thm.get_name_hint) #> Symtab.make |
31 #> map (rpair () o nickname_of) #> Symtab.make |
32 |
32 |
33 fun evaluate_mash_suggestions ctxt params thy file_name = |
33 fun evaluate_mash_suggestions ctxt params thy file_name = |
34 let |
34 let |
35 val {provers, max_facts, slice, type_enc, lam_trans, timeout, ...} = |
35 val {provers, max_facts, slice, type_enc, lam_trans, timeout, ...} = |
36 Sledgehammer_Isar.default_params ctxt [] |
36 Sledgehammer_Isar.default_params ctxt [] |
68 end |
68 end |
69 fun solve_goal (j, line) = |
69 fun solve_goal (j, line) = |
70 let |
70 let |
71 val (name, suggs) = extract_query line |
71 val (name, suggs) = extract_query line |
72 val th = |
72 val th = |
73 case find_first (fn (_, th) => Thm.get_name_hint th = name) facts of |
73 case find_first (fn (_, th) => nickname_of th = name) facts of |
74 SOME (_, th) => th |
74 SOME (_, th) => th |
75 | NONE => error ("No fact called \"" ^ name ^ "\"") |
75 | NONE => error ("No fact called \"" ^ name ^ "\"") |
76 val goal = goal_of_thm thy th |
76 val goal = goal_of_thm thy th |
77 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 |
77 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 |
78 val isar_deps = isabelle_dependencies_of all_names th |
78 val isar_deps = isabelle_dependencies_of all_names th |