# HG changeset patch
# User wenzelm
# Date 925488603 -7200
# Node ID daa00919502b8705cadc70aa81260e54117fe116
# Parent  17b7b88a8e3cdf6f9728303b956121da789cb949
theory data: copy;

diff -r 17b7b88a8e3c -r daa00919502b src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Fri Apr 30 18:09:33 1999 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Fri Apr 30 18:10:03 1999 +0200
@@ -86,6 +86,7 @@
   type T = datatype_info Symtab.table;
 
   val empty = Symtab.empty;
+  val copy = I;
   val prep_ext = I;
   val merge: T * T -> T = Symtab.merge (K true);
 
diff -r 17b7b88a8e3c -r daa00919502b src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Fri Apr 30 18:09:33 1999 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Fri Apr 30 18:10:03 1999 +0200
@@ -161,6 +161,7 @@
   type T = inductive_info Symtab.table;
 
   val empty = Symtab.empty;
+  val copy = I;
   val prep_ext = I;
   val merge: T * T -> T = Symtab.merge (K true);
 
diff -r 17b7b88a8e3c -r daa00919502b src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Fri Apr 30 18:09:33 1999 +0200
+++ b/src/HOL/Tools/record_package.ML	Fri Apr 30 18:10:03 1999 +0200
@@ -338,6 +338,7 @@
       (thm Symtab.table * Simplifier.simpset);          (*field split rules*)
 
   val empty = (Symtab.empty, (Symtab.empty, HOL_basic_ss));
+  val copy = I;
   val prep_ext = I;
   fun merge ((recs1, (sps1, ss1)), (recs2, (sps2, ss2))) =
     (Symtab.merge (K true) (recs1, recs2),
diff -r 17b7b88a8e3c -r daa00919502b src/Provers/classical.ML
--- a/src/Provers/classical.ML	Fri Apr 30 18:09:33 1999 +0200
+++ b/src/Provers/classical.ML	Fri Apr 30 18:10:03 1999 +0200
@@ -31,7 +31,7 @@
   val clasetK: Object.kind
   exception ClasetData of Object.T ref
   val setup: (theory -> theory) list
-  val fix_methods: Object.T * (Object.T -> Object.T) *
+  val fix_methods: Object.T * (Object.T -> Object.T) * (Object.T -> Object.T) *
     (Object.T * Object.T -> Object.T) * (Sign.sg -> Object.T -> unit) -> unit
 end;
 
@@ -181,18 +181,20 @@
   fun undef _ = raise Match;
 
   val empty_ref = ref ERROR;
+  val copy_fn = ref (undef: Object.T -> Object.T);
   val prep_ext_fn = ref (undef: Object.T -> Object.T);
   val merge_fn = ref (undef: Object.T * Object.T -> Object.T);
   val print_fn = ref (undef: Sign.sg -> Object.T -> unit);
 
   val empty = ClasetData empty_ref;
+  fun copy exn = ! copy_fn exn;
   fun prep_ext exn = ! prep_ext_fn exn;
   fun merge exn = ! merge_fn exn;
   fun print sg exn = ! print_fn sg exn;
 in
-  val setup = [Theory.init_data clasetK (empty, prep_ext, merge, print)];
-  fun fix_methods (e, ext, mrg, prt) =
-    (empty_ref := e; prep_ext_fn := ext; merge_fn := mrg; print_fn := prt);
+  val setup = [Theory.init_data clasetK (empty, copy, prep_ext, merge, print)];
+  fun fix_methods (e, cp, ext, mrg, prt) =
+    (empty_ref := e; copy_fn := cp; prep_ext_fn := ext; merge_fn := mrg; print_fn := prt);
 end;
 
 
@@ -787,15 +789,16 @@
   val empty = CSData (ref empty_cs);
 
   (*create new references*)
-  fun prep_ext (ClasetData (ref (CSData (ref cs)))) =
+  fun copy (ClasetData (ref (CSData (ref cs)))) =
     ClasetData (ref (CSData (ref cs)));
+  val prep_ext = copy;
 
   fun merge (ClasetData (ref (CSData (ref cs1))), ClasetData (ref (CSData (ref cs2)))) =
     ClasetData (ref (CSData (ref (merge_cs (cs1, cs2)))));
 
   fun print (_: Sign.sg) (ClasetData (ref (CSData (ref cs)))) = print_cs cs;
 in
-  val _ = fix_methods (empty, prep_ext, merge, print);
+  val _ = fix_methods (empty, copy, prep_ext, merge, print);
 end;
 
 
diff -r 17b7b88a8e3c -r daa00919502b src/Provers/simplifier.ML
--- a/src/Provers/simplifier.ML	Fri Apr 30 18:09:33 1999 +0200
+++ b/src/Provers/simplifier.ML	Fri Apr 30 18:10:03 1999 +0200
@@ -266,7 +266,8 @@
   type T = simpset ref;
 
   val empty = ref empty_ss;
-  fun prep_ext (ref ss) = (ref ss): T;            (*create new reference!*)
+  fun copy (ref ss) = (ref ss): T;            (*create new reference!*)
+  val prep_ext = copy;
   fun merge (ref ss1, ref ss2) = ref (merge_ss (ss1, ss2));
   fun print _ (ref ss) = print_ss ss;
 end;
diff -r 17b7b88a8e3c -r daa00919502b src/ZF/Tools/induct_tacs.ML
--- a/src/ZF/Tools/induct_tacs.ML	Fri Apr 30 18:09:33 1999 +0200
+++ b/src/ZF/Tools/induct_tacs.ML	Fri Apr 30 18:10:03 1999 +0200
@@ -37,6 +37,7 @@
   type T = datatype_info Symtab.table;
 
   val empty = Symtab.empty;
+  val copy = I;
   val prep_ext = I;
   val merge: T * T -> T = Symtab.merge (K true);
 
@@ -63,6 +64,7 @@
   type T = constructor_info Symtab.table
 
   val empty = Symtab.empty
+  val copy = I;
   val prep_ext = I
   val merge: T * T -> T = Symtab.merge (K true)
 
diff -r 17b7b88a8e3c -r daa00919502b src/ZF/Tools/typechk.ML
--- a/src/ZF/Tools/typechk.ML	Fri Apr 30 18:09:33 1999 +0200
+++ b/src/ZF/Tools/typechk.ML	Fri Apr 30 18:10:03 1999 +0200
@@ -94,7 +94,8 @@
   val name = "ZF/type-checker";
   type T = tcset ref;
   val empty = ref (TC{rules=[], net=Net.empty});
-  fun prep_ext (ref ss) = (ref ss): T;            (*create new reference!*)
+  fun copy (ref tc) = ref tc;
+  val prep_ext = copy;
   fun merge (ref tc1, ref tc2) = ref (merge_tc (tc1, tc2));
   fun print _ (ref tc) = print_tc tc;
   end;