equal
deleted
inserted
replaced
325 |
325 |
326 fun run_minimize (params as {provers, ...}) i refs state = |
326 fun run_minimize (params as {provers, ...}) i refs state = |
327 let |
327 let |
328 val ctxt = Proof.context_of state |
328 val ctxt = Proof.context_of state |
329 val reserved = reserved_isar_keyword_table () |
329 val reserved = reserved_isar_keyword_table () |
330 val chained_ths = normalize_chained_theorems (#facts (Proof.goal state)) |
330 val chained_ths = #facts (Proof.goal state) |
331 val css_table = clasimpset_rule_table_of ctxt |
331 val css_table = clasimpset_rule_table_of ctxt |
332 val facts = |
332 val facts = |
333 refs |> maps (map (apsnd single) |
333 refs |> maps (map (apsnd single) |
334 o fact_from_ref ctxt reserved chained_ths css_table) |
334 o fact_from_ref ctxt reserved chained_ths css_table) |
335 in |
335 in |