diff -r d7b60303adb8 -r e7279efbe3dd quotient_info.ML
--- a/quotient_info.ML	Wed Nov 11 10:22:47 2009 +0100
+++ b/quotient_info.ML	Wed Nov 11 11:59:22 2009 +0100
@@ -27,12 +27,11 @@
 (* info about map- and rel-functions *)
 type maps_info = {mapfun: string, relfun: string}
 
-structure MapsData = TheoryDataFun
+structure MapsData = Theory_Data
   (type T = maps_info Symtab.table
    val empty = Symtab.empty
-   val copy = I
    val extend = I
-   fun merge _ = Symtab.merge (K true))
+   val merge = Symtab.merge (K true))
 
 val maps_lookup = Symtab.lookup o MapsData.get
 
@@ -68,12 +67,11 @@
 (* info about the quotient types *)
 type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm}
 
-structure QuotData = TheoryDataFun
+structure QuotData = Theory_Data
   (type T = quotient_info list
    val empty = []
-   val copy = I
    val extend = I
-   fun merge _ = (op @)) (* FIXME: is this the correct merging function for the list? *)
+   val merge = (op @)) (* FIXME: is this the correct merging function for the list? *)
 
 val quotdata_lookup_thy = QuotData.get
 val quotdata_lookup = QuotData.get o ProofContext.theory_of