--- a/IntEx.thy	Wed Nov 11 18:49:46 2009 +0100
+++ b/IntEx.thy	Wed Nov 11 18:51:59 2009 +0100
@@ -46,10 +46,6 @@
 term PLUS
 thm PLUS_def
 
-ML {* toplevel_pp ["typ"] "ProofDisplay.pp_typ Pure.thy"; *}
-
-ML {* prop_of @{thm PLUS_def} *}
-
 fun
   my_neg :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
 where

--- a/quotient_info.ML	Wed Nov 11 18:49:46 2009 +0100
+++ b/quotient_info.ML	Wed Nov 11 18:51:59 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