equal
deleted
inserted
replaced
73 case find_first (fn (_, th) => nickname_of 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 = isar_dependencies_of all_names th |
79 val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS) |
79 val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS) |
80 val mepo_facts = |
80 val mepo_facts = |
81 Sledgehammer_MePo.iterative_relevant_facts ctxt params prover |
81 Sledgehammer_MePo.iterative_relevant_facts ctxt params prover |
82 slack_max_facts NONE hyp_ts concl_t facts |
82 slack_max_facts NONE hyp_ts concl_t facts |
83 val mash_facts = facts |> suggested_facts suggs |
83 val mash_facts = facts |> suggested_facts suggs |