equal
deleted
inserted
replaced
177 val _ = |
177 val _ = |
178 if kind <> "" then |
178 if kind <> "" then |
179 let |
179 let |
180 val suggs = |
180 val suggs = |
181 old_facts |
181 old_facts |
182 |> Sledgehammer_MePo.iterative_relevant_facts ctxt params prover |
182 |> Sledgehammer_MePo.mepo_suggested_facts ctxt params prover |
183 max_relevant NONE hyp_ts concl_t |
183 max_relevant NONE hyp_ts concl_t |
184 |> map (fn ((name, _), _) => name ()) |
184 |> map (fn ((name, _), _) => name ()) |
185 val s = escape_meta name ^ ": " ^ escape_metas suggs ^ "\n" |
185 val s = escape_meta name ^ ": " ^ escape_metas suggs ^ "\n" |
186 in File.append path s end |
186 in File.append path s end |
187 else |
187 else |