src/HOL/Import/import.ML
changeset 33522 737589bb9bb8
parent 32970 fbd2bb2489a8
child 36945 9bec62c10714
     1.1 --- a/src/HOL/Import/import.ML	Sun Nov 08 18:43:22 2009 +0100
     1.2 +++ b/src/HOL/Import/import.ML	Sun Nov 08 18:43:42 2009 +0100
     1.3 @@ -9,13 +9,12 @@
     1.4      val setup      : theory -> theory
     1.5  end
     1.6  
     1.7 -structure ImportData = TheoryDataFun
     1.8 +structure ImportData = Theory_Data
     1.9  (
    1.10 -  type T = ProofKernel.thm option array option
    1.11 +  type T = ProofKernel.thm option array option  (* FIXME mutable array !??!!! *)
    1.12    val empty = NONE
    1.13 -  val copy = I
    1.14    val extend = I
    1.15 -  fun merge _ _ = NONE
    1.16 +  fun merge _ = NONE
    1.17  )
    1.18  
    1.19  structure Import :> IMPORT =