# HG changeset patch
# User wenzelm
# Date 1006904786 -3600
# Node ID ce5f9e61c037f660a031a9081157f2e650bb9791
# Parent  26407b087c8eac7a5019a6613bbc68560be57bbb
theory data: removed obsolete finish method;

diff -r 26407b087c8e -r ce5f9e61c037 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Wed Nov 28 00:44:37 2001 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Wed Nov 28 00:46:26 2001 +0100
@@ -94,7 +94,6 @@
 
   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 26407b087c8e -r ce5f9e61c037 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Wed Nov 28 00:44:37 2001 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Wed Nov 28 00:46:26 2001 +0100
@@ -97,7 +97,6 @@
 
   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 26407b087c8e -r ce5f9e61c037 src/HOL/Tools/primrec_package.ML
--- a/src/HOL/Tools/primrec_package.ML	Wed Nov 28 00:44:37 2001 +0100
+++ b/src/HOL/Tools/primrec_package.ML	Wed Nov 28 00:46:26 2001 +0100
@@ -47,7 +47,6 @@
 
   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 26407b087c8e -r ce5f9e61c037 src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Wed Nov 28 00:44:37 2001 +0100
+++ b/src/HOL/Tools/recdef_package.ML	Wed Nov 28 00:46:26 2001 +0100
@@ -111,7 +111,6 @@
 
   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 26407b087c8e -r ce5f9e61c037 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Wed Nov 28 00:44:37 2001 +0100
+++ b/src/HOL/Tools/record_package.ML	Wed Nov 28 00:46:26 2001 +0100
@@ -375,7 +375,6 @@
       {fields = Symtab.empty, simpset = HOL_basic_ss};
 
   val copy = I;
-  val finish = I;
   val prep_ext = I;
   fun merge
    ({records = recs1,
diff -r 26407b087c8e -r ce5f9e61c037 src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Wed Nov 28 00:44:37 2001 +0100
+++ b/src/HOL/arith_data.ML	Wed Nov 28 00:46:26 2001 +0100
@@ -213,7 +213,6 @@
 
   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 26407b087c8e -r ce5f9e61c037 src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Wed Nov 28 00:44:37 2001 +0100
+++ b/src/Provers/Arith/fast_lin_arith.ML	Wed Nov 28 00:46:26 2001 +0100
@@ -100,7 +100,6 @@
   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 26407b087c8e -r ce5f9e61c037 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Wed Nov 28 00:44:37 2001 +0100
+++ b/src/Provers/classical.ML	Wed Nov 28 00:46:26 2001 +0100
@@ -922,7 +922,6 @@
 
   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 26407b087c8e -r ce5f9e61c037 src/Provers/simplifier.ML
--- a/src/Provers/simplifier.ML	Wed Nov 28 00:44:37 2001 +0100
+++ b/src/Provers/simplifier.ML	Wed Nov 28 00:46:26 2001 +0100
@@ -312,7 +312,6 @@
 
   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 26407b087c8e -r ce5f9e61c037 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Wed Nov 28 00:44:37 2001 +0100
+++ b/src/Pure/Isar/attrib.ML	Wed Nov 28 00:46:26 2001 +0100
@@ -56,7 +56,6 @@
 
   val empty = {space = NameSpace.empty, attrs = Symtab.empty};
   val copy = I;
-  val finish = I;
   val prep_ext = I;
 
   fun merge ({space = space1, attrs = attrs1}, {space = space2, attrs = attrs2}) =
diff -r 26407b087c8e -r ce5f9e61c037 src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Wed Nov 28 00:44:37 2001 +0100
+++ b/src/Pure/Isar/calculation.ML	Wed Nov 28 00:46:26 2001 +0100
@@ -40,7 +40,6 @@
 
   val empty = NetRules.elim;
   val copy = I;
-  val finish = I;
   val prep_ext = I;
   val merge = NetRules.merge;
   val print = print_rules Display.pretty_thm_sg;
diff -r 26407b087c8e -r ce5f9e61c037 src/Pure/Isar/induct_attrib.ML
--- a/src/Pure/Isar/induct_attrib.ML	Wed Nov 28 00:44:37 2001 +0100
+++ b/src/Pure/Isar/induct_attrib.ML	Wed Nov 28 00:46:26 2001 +0100
@@ -110,7 +110,6 @@
     ((init_rules (first_var o #2), init_rules (Thm.major_prem_of o #2)),
      (init_rules (last_var o #2), init_rules (Thm.major_prem_of o #2)));
   val copy = I;
-  val finish = I;
   val prep_ext = I;
   fun merge (((casesT1, casesS1), (inductT1, inductS1)),
       ((casesT2, casesS2), (inductT2, inductS2))) =
diff -r 26407b087c8e -r ce5f9e61c037 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Wed Nov 28 00:44:37 2001 +0100
+++ b/src/Pure/Isar/method.ML	Wed Nov 28 00:46:26 2001 +0100
@@ -176,7 +176,6 @@
 
   val empty = [NetRules.intro, NetRules.elim, NetRules.intro, NetRules.elim];
   val copy = I;
-  val finish = I;
   val prep_ext = I;
   fun merge x = map2 NetRules.merge x;
   val print = print_rules Display.pretty_thm_sg;
@@ -461,7 +460,6 @@
 
   val empty = {space = NameSpace.empty, meths = Symtab.empty};
   val copy = I;
-  val finish = I;
   val prep_ext = I;
   fun merge ({space = space1, meths = meths1}, {space = space2, meths = meths2}) =
     {space = NameSpace.merge (space1, space2),
diff -r 26407b087c8e -r ce5f9e61c037 src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Wed Nov 28 00:44:37 2001 +0100
+++ b/src/Pure/Isar/object_logic.ML	Wed Nov 28 00:46:26 2001 +0100
@@ -40,7 +40,6 @@
 
   val empty = (None, ([], [Drule.norm_hhf_eq]));
   val copy = I;
-  val finish = I;
   val prep_ext = I;
 
   fun merge_judgment (Some x, Some y) =
diff -r 26407b087c8e -r ce5f9e61c037 src/Pure/Isar/rule_context.ML
--- a/src/Pure/Isar/rule_context.ML	Wed Nov 28 00:44:37 2001 +0100
+++ b/src/Pure/Isar/rule_context.ML	Wed Nov 28 00:46:26 2001 +0100
@@ -115,7 +115,6 @@
 
   val empty = empty_rules;
   val copy = I;
-  val finish = I;
   val prep_ext = I;
 
   fun merge (Rules {rules = rules1, wrappers = wrappers1, ...},
diff -r 26407b087c8e -r ce5f9e61c037 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Wed Nov 28 00:44:37 2001 +0100
+++ b/src/Pure/Thy/present.ML	Wed Nov 28 00:46:26 2001 +0100
@@ -78,7 +78,6 @@
 
   val empty = {name = "Pure", session = [], is_local = false};
   val copy = I;
-  val finish = I;
   fun prep_ext _ = {name = "", session = [], is_local = false};
   fun merge _ = empty;
   fun print _ _ = ();
diff -r 26407b087c8e -r ce5f9e61c037 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Wed Nov 28 00:44:37 2001 +0100
+++ b/src/Pure/axclass.ML	Wed Nov 28 00:46:26 2001 +0100
@@ -172,7 +172,6 @@
 
   val empty = Symtab.empty;
   val copy = I;
-  val finish = I;
   val prep_ext = I;
   fun merge (tab1, tab2) = Symtab.merge (K true) (tab1, tab2);
 
diff -r 26407b087c8e -r ce5f9e61c037 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Wed Nov 28 00:44:37 2001 +0100
+++ b/src/Pure/codegen.ML	Wed Nov 28 00:46:26 2001 +0100
@@ -82,7 +82,6 @@
 
   val empty = {codegens = [], consts = [], types = []};
   val copy = I;
-  val finish = I;
   val prep_ext = I;
 
   fun merge ({codegens = codegens1, consts = consts1, types = types1},
diff -r 26407b087c8e -r ce5f9e61c037 src/Pure/goals.ML
--- a/src/Pure/goals.ML	Wed Nov 28 00:44:37 2001 +0100
+++ b/src/Pure/goals.ML	Wed Nov 28 00:46:26 2001 +0100
@@ -192,7 +192,6 @@
 
   val empty = make_locale_data NameSpace.empty Symtab.empty (ref []);
   fun copy {space, locales, scope = ref locs} = make_locale_data space locales (ref locs);
-  val finish = I;
   fun prep_ext {space, locales, scope = _} = make_locale_data space locales (ref []);
   fun merge ({space = space1, locales = locales1, scope = _},
     {space = space2, locales = locales2, scope = _}) =
diff -r 26407b087c8e -r ce5f9e61c037 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Wed Nov 28 00:44:37 2001 +0100
+++ b/src/Pure/proofterm.ML	Wed Nov 28 00:46:26 2001 +0100
@@ -1048,7 +1048,6 @@
 
   val empty = ([], []);
   val copy = I;
-  val finish = I;
   val prep_ext = I;
   fun merge ((rules1, procs1), (rules2, procs2)) =
     (merge_lists rules1 rules2, merge_alists procs1 procs2);
diff -r 26407b087c8e -r ce5f9e61c037 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Wed Nov 28 00:44:37 2001 +0100
+++ b/src/Pure/pure_thy.ML	Wed Nov 28 00:46:26 2001 +0100
@@ -83,7 +83,6 @@
 
   val empty = mk_empty ();
   fun copy (ref x) = ref x;
-  val finish = I;
   val prep_ext = mk_empty;
   val merge = mk_empty;
 
@@ -390,7 +389,6 @@
 
   val empty = {name = "", version = 0};
   val copy = I;
-  val finish = I;
   val prep_ext  = I;
   fun merge _ = empty;
   fun print _ _ = ();
@@ -424,7 +422,6 @@
 
 fun end_theory thy =
   thy
-  |> Theory.finish
   |> Theory.add_name (get_name thy);
 
 fun checkpoint thy =
diff -r 26407b087c8e -r ce5f9e61c037 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Wed Nov 28 00:44:37 2001 +0100
+++ b/src/Pure/theory.ML	Wed Nov 28 00:46:26 2001 +0100
@@ -86,7 +86,6 @@
   val hide_consts: string list -> theory -> theory
   val add_name: string -> theory -> theory
   val copy: theory -> theory
-  val finish: theory -> theory
   val prep_ext: theory -> theory
   val prep_ext_merge: theory list -> theory
   val requires: theory -> string -> string -> unit
@@ -98,8 +97,7 @@
 sig
   include THEORY
   val init_data: Object.kind -> (Object.T * (Object.T -> Object.T) * (Object.T -> Object.T) *
-    (Object.T -> Object.T) * (Object.T * Object.T -> Object.T) *
-    (Sign.sg -> Object.T -> unit)) -> theory -> theory
+    (Object.T * Object.T -> Object.T) * (Sign.sg -> Object.T -> unit)) -> theory -> theory
   val print_data: Object.kind -> theory -> unit
   val get_data: Object.kind -> (Object.T -> 'a) -> theory -> 'a
   val put_data: Object.kind -> ('a -> Object.T) -> 'a -> theory -> theory
@@ -229,7 +227,6 @@
 val hide_consts      = curry hide_space_i Sign.constK;
 val add_name         = ext_sign Sign.add_name;
 val copy             = ext_sign (K Sign.copy) ();
-val finish           = ext_sign (K Sign.finish) ();
 val prep_ext         = ext_sign (K Sign.prep_ext) ();
 
 
diff -r 26407b087c8e -r ce5f9e61c037 src/Pure/theory_data.ML
--- a/src/Pure/theory_data.ML	Wed Nov 28 00:44:37 2001 +0100
+++ b/src/Pure/theory_data.ML	Wed Nov 28 00:46:26 2001 +0100
@@ -11,7 +11,6 @@
   type T
   val empty: T
   val copy: T -> T
-  val finish: T -> T
   val prep_ext: T -> T
   val merge: T * T -> T
   val print: Sign.sg -> T -> unit
@@ -41,7 +40,6 @@
   Theory.init_data kind
     (Data Args.empty,
       fn (Data x) => Data (Args.copy x),
-      fn (Data x) => Data (Args.finish 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);
diff -r 26407b087c8e -r ce5f9e61c037 src/Sequents/prover.ML
--- a/src/Sequents/prover.ML	Wed Nov 28 00:44:37 2001 +0100
+++ b/src/Sequents/prover.ML	Wed Nov 28 00:46:26 2001 +0100
@@ -174,7 +174,6 @@
   type T = pack ref;
   val empty = ref empty_pack
   fun copy (ref pack) = ref pack;
-  val finish = I;
   val prep_ext = copy;
   fun merge (ref pack1, ref pack2) = ref (merge_pack (pack1, pack2));
   fun print _ (ref pack) = print_pack pack;
diff -r 26407b087c8e -r ce5f9e61c037 src/ZF/Tools/ind_cases.ML
--- a/src/ZF/Tools/ind_cases.ML	Wed Nov 28 00:44:37 2001 +0100
+++ b/src/ZF/Tools/ind_cases.ML	Wed Nov 28 00:46:26 2001 +0100
@@ -26,7 +26,6 @@
 
   val empty = Symtab.empty;
   val copy = I;
-  val finish = I;
   val prep_ext = I;
   fun merge (tab1, tab2) = Symtab.merge (K true) (tab1, tab2);
   fun print _ _ = ();
diff -r 26407b087c8e -r ce5f9e61c037 src/ZF/Tools/induct_tacs.ML
--- a/src/ZF/Tools/induct_tacs.ML	Wed Nov 28 00:44:37 2001 +0100
+++ b/src/ZF/Tools/induct_tacs.ML	Wed Nov 28 00:46:26 2001 +0100
@@ -37,7 +37,6 @@
 
   val empty = Symtab.empty;
   val copy = I;
-  val finish = I;
   val prep_ext = I;
   val merge: T * T -> T = Symtab.merge (K true);
 
@@ -65,7 +64,6 @@
 
   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 26407b087c8e -r ce5f9e61c037 src/ZF/Tools/typechk.ML
--- a/src/ZF/Tools/typechk.ML	Wed Nov 28 00:44:37 2001 +0100
+++ b/src/ZF/Tools/typechk.ML	Wed Nov 28 00:46:26 2001 +0100
@@ -127,7 +127,6 @@
   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;