79    val merge = Symtab.merge (K true)) 

    79    val merge = Symtab.merge (K true)) 

    80 

    80 

    81 val quotdata_lookup_thy = Symtab.lookup o QuotData.get

    81 val quotdata_lookup_thy = Symtab.lookup o QuotData.get

    82 val quotdata_lookup = quotdata_lookup_thy o ProofContext.theory_of

    82 val quotdata_lookup = quotdata_lookup_thy o ProofContext.theory_of

    83 

    83 

    85       QuotData.map (Symtab.update (qty_name, {qtyp = qty, rtyp = rty, rel = rel, equiv_thm = equiv_thm}))

    85       QuotData.map (Symtab.update (qty_name, {qtyp = qty, rtyp = rty, rel = rel, equiv_thm = equiv_thm}))

    86 

    86 

    87 fun quotdata_update qty_name (qty, rty, rel, equiv_thm) = 

    87 fun quotdata_update qty_name (qty, rty, rel, equiv_thm) = 

    88       ProofContext.theory (quotdata_update_thy qty_name (qty, rty, rel, equiv_thm))

    88       ProofContext.theory (quotdata_update_thy qty_name (qty, rty, rel, equiv_thm))

    89 

    89