src/HOL/Import/import.ML

--- a/src/HOL/Import/import.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Import/import.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -9,13 +9,12 @@
     val setup      : theory -> theory
 end
 
-structure ImportData = TheoryDataFun
+structure ImportData = Theory_Data
 (
-  type T = ProofKernel.thm option array option
+  type T = ProofKernel.thm option array option  (* FIXME mutable array !??!!! *)
   val empty = NONE
-  val copy = I
   val extend = I
-  fun merge _ _ = NONE
+  fun merge _ = NONE
 )
 
 structure Import :> IMPORT =