equal
deleted
inserted
replaced
77 (type T = quotient_info Symtab.table |
77 (type T = quotient_info Symtab.table |
78 val empty = Symtab.empty |
78 val empty = Symtab.empty |
79 val extend = I |
79 val extend = I |
80 val merge = Symtab.merge (K true)) |
80 val merge = Symtab.merge (K true)) |
81 |
81 |
82 val quotdata_lookup_thy = Symtab.lookup o QuotData.get |
82 fun quotdata_lookup_thy thy str = |
|
83 Symtab.lookup (QuotData.get thy) (Sign.intern_type thy str) |
|
84 |
83 val quotdata_lookup = quotdata_lookup_thy o ProofContext.theory_of |
85 val quotdata_lookup = quotdata_lookup_thy o ProofContext.theory_of |
84 |
86 |
85 fun quotdata_update_thy qty_name (qty, rty, rel, equiv_thm) = |
87 fun quotdata_update_thy qty_name (qty, rty, rel, equiv_thm) = |
86 QuotData.map (Symtab.update (qty_name, {qtyp = qty, rtyp = rty, rel = rel, equiv_thm = equiv_thm})) |
88 QuotData.map (Symtab.update (qty_name, {qtyp = qty, rtyp = rty, rel = rel, equiv_thm = equiv_thm})) |
87 |
89 |