equal
deleted
inserted
replaced
428 val empty = Symtab.empty; |
428 val empty = Symtab.empty; |
429 val extend = I; |
429 val extend = I; |
430 val merge = Symtab.merge eq_bnf; |
430 val merge = Symtab.merge eq_bnf; |
431 ); |
431 ); |
432 |
432 |
433 val bnf_of = Symtab.lookup o Data.get o Context.Proof; |
433 fun bnf_of ctxt str = |
|
434 Symtab.lookup (Data.get (Context.Proof ctxt)) str |
|
435 |> Option.map (morph_bnf (Morphism.thm_morphism (Thm.transfer (Proof_Context.theory_of ctxt)))); |
434 |
436 |
435 |
437 |
436 |
438 |
437 (* Utilities *) |
439 (* Utilities *) |
438 |
440 |