src/HOL/Tools/datatype_package.ML
changeset 6556 daa00919502b
parent 6479 b0448cab1b1e
child 6723 f342449d73ca
equal deleted inserted replaced
6555:17b7b88a8e3c 6556:daa00919502b
    84 struct
    84 struct
    85   val name = "HOL/datatypes";
    85   val name = "HOL/datatypes";
    86   type T = datatype_info Symtab.table;
    86   type T = datatype_info Symtab.table;
    87 
    87 
    88   val empty = Symtab.empty;
    88   val empty = Symtab.empty;
       
    89   val copy = I;
    89   val prep_ext = I;
    90   val prep_ext = I;
    90   val merge: T * T -> T = Symtab.merge (K true);
    91   val merge: T * T -> T = Symtab.merge (K true);
    91 
    92 
    92   fun print sg tab =
    93   fun print sg tab =
    93     Pretty.writeln (Pretty.strs ("datatypes:" ::
    94     Pretty.writeln (Pretty.strs ("datatypes:" ::