--- a/src/Pure/theory_data.ML Fri Apr 30 17:59:36 1999 +0200
+++ b/src/Pure/theory_data.ML Fri Apr 30 18:01:11 1999 +0200
@@ -10,6 +10,7 @@
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
@@ -37,6 +38,7 @@
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);