src/HOL/Tools/Datatype/datatype.ML
changeset 33522 737589bb9bb8
parent 33368 b1cf34f1855c
child 33955 fff6f11b1f09
     1.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Sun Nov 08 18:43:22 2009 +0100
     1.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Sun Nov 08 18:43:42 2009 +0100
     1.3 @@ -42,7 +42,7 @@
     1.4  
     1.5  (* data management *)
     1.6  
     1.7 -structure DatatypesData = TheoryDataFun
     1.8 +structure DatatypesData = Theory_Data
     1.9  (
    1.10    type T =
    1.11      {types: info Symtab.table,
    1.12 @@ -51,11 +51,10 @@
    1.13  
    1.14    val empty =
    1.15      {types = Symtab.empty, constrs = Symtab.empty, cases = Symtab.empty};
    1.16 -  val copy = I;
    1.17    val extend = I;
    1.18 -  fun merge _
    1.19 +  fun merge
    1.20      ({types = types1, constrs = constrs1, cases = cases1},
    1.21 -     {types = types2, constrs = constrs2, cases = cases2}) =
    1.22 +     {types = types2, constrs = constrs2, cases = cases2}) : T =
    1.23      {types = Symtab.merge (K true) (types1, types2),
    1.24       constrs = Symtab.join (K (AList.merge (op =) (K true))) (constrs1, constrs2),
    1.25       cases = Symtab.merge (K true) (cases1, cases2)};