equal
deleted
inserted
replaced
275 |
275 |
276 local |
276 local |
277 |
277 |
278 fun lookup_rule which ctxt = |
278 fun lookup_rule which ctxt = |
279 AList.lookup (op =) (Item_Net.content (which (get_local ctxt))) |
279 AList.lookup (op =) (Item_Net.content (which (get_local ctxt))) |
280 #> Option.map (Thm.transfer (Proof_Context.theory_of ctxt)); |
280 #> Option.map (Thm.transfer' ctxt); |
281 |
281 |
282 fun find_rules which how ctxt x = |
282 fun find_rules which how ctxt x = |
283 Item_Net.retrieve (which (get_local ctxt)) (how x) |
283 Item_Net.retrieve (which (get_local ctxt)) (how x) |
284 |> map (Thm.transfer (Proof_Context.theory_of ctxt) o snd); |
284 |> map (Thm.transfer' ctxt o snd); |
285 |
285 |
286 in |
286 in |
287 |
287 |
288 val lookup_casesT = lookup_rule (#1 o #1); |
288 val lookup_casesT = lookup_rule (#1 o #1); |
289 val lookup_casesP = lookup_rule (#2 o #1); |
289 val lookup_casesP = lookup_rule (#2 o #1); |