dropped copy operation for legacy TheoryDataFun

--- a/src/Pure/axclass.ML	Mon Jan 04 14:09:56 2010 +0100
+++ b/src/Pure/axclass.ML	Mon Jan 04 14:09:56 2010 +0100
@@ -118,7 +118,6 @@
 (
   type T = axclasses * (instances * inst_params);
   val empty = ((Symtab.empty, []), (([], Symtab.empty), (Symtab.empty, Symtab.empty)));
-  val copy = I;
   val extend = I;
   fun merge pp ((axclasses1, (instances1, inst_params1)), (axclasses2, (instances2, inst_params2))) =
     (merge_axclasses pp (axclasses1, axclasses2),

--- a/src/Pure/context.ML	Mon Jan 04 14:09:56 2010 +0100
+++ b/src/Pure/context.ML	Mon Jan 04 14:09:56 2010 +0100
@@ -83,7 +83,7 @@
   include CONTEXT
   structure Theory_Data:
   sig
-    val declare: Object.T -> (Object.T -> Object.T) -> (Object.T -> Object.T) ->
+    val declare: Object.T -> (Object.T -> Object.T) ->
       (Pretty.pp -> Object.T * Object.T -> Object.T) -> serial
     val get: serial -> (Object.T -> 'a) -> theory -> 'a
     val put: serial -> ('a -> Object.T) -> 'a -> theory -> theory
@@ -112,7 +112,6 @@
 
 type kind =
  {empty: Object.T,
-  copy: Object.T -> Object.T,
   extend: Object.T -> Object.T,
   merge: Pretty.pp -> Object.T * Object.T -> Object.T};
 
@@ -126,18 +125,16 @@
 in
 
 fun invoke_empty k = invoke (K o #empty) k ();
-val invoke_copy = invoke #copy;
 val invoke_extend = invoke #extend;
 fun invoke_merge pp = invoke (fn kind => #merge kind pp);
 
-fun declare_theory_data empty copy extend merge =
+fun declare_theory_data empty extend merge =
   let
     val k = serial ();
-    val kind = {empty = empty, copy = copy, extend = extend, merge = merge};
+    val kind = {empty = empty, extend = extend, merge = merge};
     val _ = CRITICAL (fn () => Unsynchronized.change kinds (Datatab.update (k, kind)));
   in k end;
 
-val copy_data = Datatab.map' invoke_copy;
 val extend_data = Datatab.map' invoke_extend;
 
 fun merge_data pp (data1, data2) =
@@ -341,7 +338,7 @@
     val (self', data', ancestry') =
       if draft then (self, data, ancestry)    (*destructive change!*)
       else if #stage history > 0
-      then (NONE, copy_data data, ancestry)
+      then (NONE, data, ancestry)
       else (NONE, extend_data data, make_ancestry [thy] (extend_ancestors_of thy));
     val ids' = insert_id draft id ids;
     val data'' = f data';
@@ -357,9 +354,8 @@
   let
     val Theory ({draft, id, ids, ...}, data, ancestry, history) = thy;
     val ids' = insert_id draft id ids;
-    val data' = copy_data data;
     val thy' = SYNCHRONIZED (fn () =>
-      (check_thy thy; create_thy NONE true ids' data' ancestry history));
+      (check_thy thy; create_thy NONE true ids' data ancestry history));
   in thy' end;
 
 val pre_pure_thy = create_thy NONE true Inttab.empty
@@ -430,9 +426,9 @@
 val declare = declare_theory_data;
 
 fun get k dest thy =
-  dest ((case Datatab.lookup (data_of thy) k of
+  dest (case Datatab.lookup (data_of thy) k of
     SOME x => x
-  | NONE => invoke_copy k (invoke_empty k)));   (*adhoc value*)
+  | NONE => invoke_empty k);   (*adhoc value*)
 
 fun put k mk x = modify_thy (Datatab.update (k, mk x));
 
@@ -582,7 +578,6 @@
 sig
   type T
   val empty: T
-  val copy: T -> T
   val extend: T -> T
   val merge: Pretty.pp -> T * T -> T
 end;
@@ -604,7 +599,6 @@
 
 val kind = Context.Theory_Data.declare
   (Data Data.empty)
-  (fn Data x => Data (Data.copy x))
   (fn Data x => Data (Data.extend x))
   (fn pp => fn (Data x1, Data x2) => Data (Data.merge pp (x1, x2)));
 
@@ -639,7 +633,6 @@
 (
   type T = Data.T;
   val empty = Data.empty;
-  val copy = I;
   val extend = Data.extend;
   fun merge _ = Data.merge;
 );

--- a/src/Pure/sign.ML	Mon Jan 04 14:09:56 2010 +0100
+++ b/src/Pure/sign.ML	Mon Jan 04 14:09:56 2010 +0100
@@ -151,7 +151,6 @@
 structure SignData = TheoryDataFun
 (
   type T = sign;
-  val copy = I;
   fun extend (Sign {syn, tsig, consts, ...}) =
     make_sign (Name_Space.default_naming, syn, tsig, consts);
 

--- a/src/Pure/theory.ML	Mon Jan 04 14:09:56 2010 +0100
+++ b/src/Pure/theory.ML	Mon Jan 04 14:09:56 2010 +0100
@@ -91,7 +91,6 @@
   type T = thy;
   val empty_axioms = Name_Space.empty_table "axiom" : term Name_Space.table;
   val empty = make_thy (empty_axioms, Defs.empty, ([], []));
-  val copy = I;
 
   fun extend (Thy {axioms = _, defs, wrappers}) = make_thy (empty_axioms, defs, wrappers);