# HG changeset patch
# User wenzelm
# Date 1005260377 -3600
# Node ID bd6eb9194a5d95cfc202d0f3b081a82d5b87f52a
# Parent  b6f10dcde8037ff34afa86ea82c20a3c3cdf2a05
theory data: finish method;

diff -r b6f10dcde803 -r bd6eb9194a5d src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Thu Nov 08 23:57:22 2001 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Thu Nov 08 23:59:37 2001 +0100
@@ -94,6 +94,7 @@
 
   val empty = Symtab.empty;
   val copy = I;
+  val finish = I;
   val prep_ext = I;
   val merge: T * T -> T = Symtab.merge (K true);
 
diff -r b6f10dcde803 -r bd6eb9194a5d src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Thu Nov 08 23:57:22 2001 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Thu Nov 08 23:59:37 2001 +0100
@@ -98,6 +98,7 @@
 
   val empty = (Symtab.empty, []);
   val copy = I;
+  val finish = I;
   val prep_ext = I;
   fun merge ((tab1, monos1), (tab2, monos2)) =
     (Symtab.merge (K true) (tab1, tab2), Drule.merge_rules (monos1, monos2));
diff -r b6f10dcde803 -r bd6eb9194a5d src/HOL/Tools/primrec_package.ML
--- a/src/HOL/Tools/primrec_package.ML	Thu Nov 08 23:57:22 2001 +0100
+++ b/src/HOL/Tools/primrec_package.ML	Thu Nov 08 23:59:37 2001 +0100
@@ -47,6 +47,7 @@
 
   val empty = Symtab.empty;
   val copy = I;
+  val finish = I;
   val prep_ext = I;
   val merge: T * T -> T = Symtab.merge (K true);
 
diff -r b6f10dcde803 -r bd6eb9194a5d src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Thu Nov 08 23:57:22 2001 +0100
+++ b/src/HOL/Tools/recdef_package.ML	Thu Nov 08 23:59:37 2001 +0100
@@ -111,6 +111,7 @@
 
   val empty = (Symtab.empty, mk_hints ([], [], [])): T;
   val copy = I;
+  val finish = I;
   val prep_ext = I;
   fun merge
    ((tab1, {simps = simps1, congs = congs1, wfs = wfs1}),
diff -r b6f10dcde803 -r bd6eb9194a5d src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Thu Nov 08 23:57:22 2001 +0100
+++ b/src/HOL/Tools/record_package.ML	Thu Nov 08 23:59:37 2001 +0100
@@ -364,6 +364,7 @@
       {fields = Symtab.empty, simpset = HOL_basic_ss};
 
   val copy = I;
+  val finish = I;
   val prep_ext = I;
   fun merge
    ({records = recs1,
diff -r b6f10dcde803 -r bd6eb9194a5d src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Thu Nov 08 23:57:22 2001 +0100
+++ b/src/HOL/arith_data.ML	Thu Nov 08 23:59:37 2001 +0100
@@ -213,6 +213,7 @@
 
   val empty = {splits = [], inj_consts = [], discrete = []};
   val copy = I;
+  val finish = I;
   val prep_ext = I;
   fun merge ({splits= splits1, inj_consts= inj_consts1, discrete= discrete1},
              {splits= splits2, inj_consts= inj_consts2, discrete= discrete2}) =
diff -r b6f10dcde803 -r bd6eb9194a5d src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Thu Nov 08 23:57:22 2001 +0100
+++ b/src/Provers/Arith/fast_lin_arith.ML	Thu Nov 08 23:59:37 2001 +0100
@@ -100,6 +100,7 @@
   val empty = {add_mono_thms = [], mult_mono_thms = [], inj_thms = [],
                lessD = [], simpset = Simplifier.empty_ss};
   val copy = I;
+  val finish = I;
   val prep_ext = I;
 
   fun merge ({add_mono_thms= add_mono_thms1, mult_mono_thms= mult_mono_thms1, inj_thms= inj_thms1,
diff -r b6f10dcde803 -r bd6eb9194a5d src/Provers/classical.ML
--- a/src/Provers/classical.ML	Thu Nov 08 23:57:22 2001 +0100
+++ b/src/Provers/classical.ML	Thu Nov 08 23:59:37 2001 +0100
@@ -922,6 +922,7 @@
 
   val empty = ref empty_cs;
   fun copy (ref cs) = (ref cs): T;            (*create new reference!*)
+  val finish = I;
   val prep_ext = copy;
   fun merge (ref cs1, ref cs2) = ref (merge_cs (cs1, cs2));
   fun print _ (ref cs) = print_cs cs;
diff -r b6f10dcde803 -r bd6eb9194a5d src/Provers/simplifier.ML
--- a/src/Provers/simplifier.ML	Thu Nov 08 23:57:22 2001 +0100
+++ b/src/Provers/simplifier.ML	Thu Nov 08 23:59:37 2001 +0100
@@ -313,6 +313,7 @@
 
   val empty = ref empty_ss;
   fun copy (ref ss) = (ref ss): T;            (*create new reference!*)
+  val finish = I;
   val prep_ext = copy;
   fun merge (ref ss1, ref ss2) = ref (merge_ss (ss1, ss2));
   fun print _ (ref ss) = print_ss ss;
diff -r b6f10dcde803 -r bd6eb9194a5d src/ZF/Tools/induct_tacs.ML
--- a/src/ZF/Tools/induct_tacs.ML	Thu Nov 08 23:57:22 2001 +0100
+++ b/src/ZF/Tools/induct_tacs.ML	Thu Nov 08 23:59:37 2001 +0100
@@ -38,6 +38,7 @@
 
   val empty = Symtab.empty;
   val copy = I;
+  val finish = I;
   val prep_ext = I;
   val merge: T * T -> T = Symtab.merge (K true);
 
@@ -65,6 +66,7 @@
 
   val empty = Symtab.empty
   val copy = I;
+  val finish = I;
   val prep_ext = I
   val merge: T * T -> T = Symtab.merge (K true)
 
diff -r b6f10dcde803 -r bd6eb9194a5d src/ZF/Tools/typechk.ML
--- a/src/ZF/Tools/typechk.ML	Thu Nov 08 23:57:22 2001 +0100
+++ b/src/ZF/Tools/typechk.ML	Thu Nov 08 23:59:37 2001 +0100
@@ -95,6 +95,7 @@
   type T = tcset ref;
   val empty = ref (TC{rules=[], net=Net.empty});
   fun copy (ref tc) = ref tc;
+  val finish = I;
   val prep_ext = copy;
   fun merge (ref tc1, ref tc2) = ref (merge_tc (tc1, tc2));
   fun print _ (ref tc) = print_tc tc;