src/Tools/Code/code_target.ML
changeset 33522 737589bb9bb8
parent 32966 5b21661fe618
child 33969 1e7ca47c6c3d
     1.1 --- a/src/Tools/Code/code_target.ML	Sun Nov 08 18:43:22 2009 +0100
     1.2 +++ b/src/Tools/Code/code_target.ML	Sun Nov 08 18:43:42 2009 +0100
     1.3 @@ -148,13 +148,12 @@
     1.4    else
     1.5      error ("Incompatible serializers: " ^ quote target);
     1.6  
     1.7 -structure CodeTargetData = TheoryDataFun
     1.8 +structure CodeTargetData = Theory_Data
     1.9  (
    1.10    type T = target Symtab.table * string list;
    1.11    val empty = (Symtab.empty, []);
    1.12 -  val copy = I;
    1.13    val extend = I;
    1.14 -  fun merge _ ((target1, exc1) : T, (target2, exc2)) =
    1.15 +  fun merge ((target1, exc1), (target2, exc2)) : T =
    1.16      (Symtab.join (merge_target true) (target1, target2), Library.merge (op =) (exc1, exc2));
    1.17  );
    1.18