equal
deleted
inserted
replaced
457 val merge = Symtab.merge eq_bnf; |
457 val merge = Symtab.merge eq_bnf; |
458 ); |
458 ); |
459 |
459 |
460 fun bnf_of ctxt = |
460 fun bnf_of ctxt = |
461 Symtab.lookup (Data.get (Context.Proof ctxt)) |
461 Symtab.lookup (Data.get (Context.Proof ctxt)) |
462 #> Option.map (morph_bnf (Morphism.thm_morphism (Thm.transfer (Proof_Context.theory_of ctxt)))); |
462 #> Option.map (morph_bnf (Morphism.transfer_morphism (Proof_Context.theory_of ctxt))); |
463 |
463 |
464 |
464 |
465 (* Utilities *) |
465 (* Utilities *) |
466 |
466 |
467 fun normalize_set insts instA set = |
467 fun normalize_set insts instA set = |