src/HOL/Tools/Quotient/quotient_info.ML
changeset 74561 8e6c973003c8
parent 69593 3dda49e08b9d
equal deleted inserted replaced
74560:5c8177fd1295 74561:8e6c973003c8
    79     quotmaps Symtab.table *
    79     quotmaps Symtab.table *
    80     abs_rep Symtab.table *
    80     abs_rep Symtab.table *
    81     quotients Symtab.table *
    81     quotients Symtab.table *
    82     quotconsts list Symtab.table
    82     quotconsts list Symtab.table
    83   val empty: T = (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty)
    83   val empty: T = (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty)
    84   val extend = I
       
    85   fun merge
    84   fun merge
    86    ((quotmaps1, abs_rep1, quotients1, quotconsts1),
    85    ((quotmaps1, abs_rep1, quotients1, quotconsts1),
    87     (quotmaps2, abs_rep2, quotients2, quotconsts2)) : T =
    86     (quotmaps2, abs_rep2, quotients2, quotconsts2)) : T =
    88    (Symtab.merge (K true) (quotmaps1, quotmaps2),
    87    (Symtab.merge (K true) (quotmaps1, quotmaps2),
    89     Symtab.merge (K true) (abs_rep1, abs_rep2),
    88     Symtab.merge (K true) (abs_rep1, abs_rep2),