src/Pure/theory_data.ML

 signature THEORY_DATA_ARGS =
 sig
   val name: string
   type T
   val empty: T
+  val copy: T -> T
   val prep_ext: T -> T
   val merge: T * T -> T
   val print: Sign.sg -> T -> unit
 end;
 

 exception Data of T;
 
 val init =
   Theory.init_data kind
     (Data Args.empty,
+      fn (Data x) => Data (Args.copy x),
       fn (Data x) => Data (Args.prep_ext x),
       fn (Data x1, Data x2) => Data (Args.merge (x1, x2)),
       fn sg => fn (Data x) => Args.print sg x);
 
 val print = Theory.print_data kind;