--- a/src/HOL/Tools/Datatype/datatype.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML Sun Nov 08 18:43:42 2009 +0100
@@ -42,7 +42,7 @@
(* data management *)
-structure DatatypesData = TheoryDataFun
+structure DatatypesData = Theory_Data
(
type T =
{types: info Symtab.table,
@@ -51,11 +51,10 @@
val empty =
{types = Symtab.empty, constrs = Symtab.empty, cases = Symtab.empty};
- val copy = I;
val extend = I;
- fun merge _
+ fun merge
({types = types1, constrs = constrs1, cases = cases1},
- {types = types2, constrs = constrs2, cases = cases2}) =
+ {types = types2, constrs = constrs2, cases = cases2}) : T =
{types = Symtab.merge (K true) (types1, types2),
constrs = Symtab.join (K (AList.merge (op =) (K true))) (constrs1, constrs2),
cases = Symtab.merge (K true) (cases1, cases2)};