theory data: removed obsolete finish method;
authorwenzelm
Wed Nov 28 00:46:26 2001 +0100 (2001-11-28 ago)
changeset 12311ce5f9e61c037
parent 12310 26407b087c8e
child 12312 f0f06950820d
theory data: removed obsolete finish method;
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/primrec_package.ML
src/HOL/Tools/recdef_package.ML
src/HOL/Tools/record_package.ML
src/HOL/arith_data.ML
src/Provers/Arith/fast_lin_arith.ML
src/Provers/classical.ML
src/Provers/simplifier.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/calculation.ML
src/Pure/Isar/induct_attrib.ML
src/Pure/Isar/method.ML
src/Pure/Isar/object_logic.ML
src/Pure/Isar/rule_context.ML
src/Pure/Thy/present.ML
src/Pure/axclass.ML
src/Pure/codegen.ML
src/Pure/goals.ML
src/Pure/proofterm.ML
src/Pure/pure_thy.ML
src/Pure/theory.ML
src/Pure/theory_data.ML
src/Sequents/prover.ML
src/ZF/Tools/ind_cases.ML
src/ZF/Tools/induct_tacs.ML
src/ZF/Tools/typechk.ML
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Wed Nov 28 00:44:37 2001 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Wed Nov 28 00:46:26 2001 +0100
     1.3 @@ -94,7 +94,6 @@
     1.4  
     1.5    val empty = Symtab.empty;
     1.6    val copy = I;
     1.7 -  val finish = I;
     1.8    val prep_ext = I;
     1.9    val merge: T * T -> T = Symtab.merge (K true);
    1.10  
     2.1 --- a/src/HOL/Tools/inductive_package.ML	Wed Nov 28 00:44:37 2001 +0100
     2.2 +++ b/src/HOL/Tools/inductive_package.ML	Wed Nov 28 00:46:26 2001 +0100
     2.3 @@ -97,7 +97,6 @@
     2.4  
     2.5    val empty = (Symtab.empty, []);
     2.6    val copy = I;
     2.7 -  val finish = I;
     2.8    val prep_ext = I;
     2.9    fun merge ((tab1, monos1), (tab2, monos2)) =
    2.10      (Symtab.merge (K true) (tab1, tab2), Drule.merge_rules (monos1, monos2));
     3.1 --- a/src/HOL/Tools/primrec_package.ML	Wed Nov 28 00:44:37 2001 +0100
     3.2 +++ b/src/HOL/Tools/primrec_package.ML	Wed Nov 28 00:46:26 2001 +0100
     3.3 @@ -47,7 +47,6 @@
     3.4  
     3.5    val empty = Symtab.empty;
     3.6    val copy = I;
     3.7 -  val finish = I;
     3.8    val prep_ext = I;
     3.9    val merge: T * T -> T = Symtab.merge (K true);
    3.10  
     4.1 --- a/src/HOL/Tools/recdef_package.ML	Wed Nov 28 00:44:37 2001 +0100
     4.2 +++ b/src/HOL/Tools/recdef_package.ML	Wed Nov 28 00:46:26 2001 +0100
     4.3 @@ -111,7 +111,6 @@
     4.4  
     4.5    val empty = (Symtab.empty, mk_hints ([], [], [])): T;
     4.6    val copy = I;
     4.7 -  val finish = I;
     4.8    val prep_ext = I;
     4.9    fun merge
    4.10     ((tab1, {simps = simps1, congs = congs1, wfs = wfs1}),
     5.1 --- a/src/HOL/Tools/record_package.ML	Wed Nov 28 00:44:37 2001 +0100
     5.2 +++ b/src/HOL/Tools/record_package.ML	Wed Nov 28 00:46:26 2001 +0100
     5.3 @@ -375,7 +375,6 @@
     5.4        {fields = Symtab.empty, simpset = HOL_basic_ss};
     5.5  
     5.6    val copy = I;
     5.7 -  val finish = I;
     5.8    val prep_ext = I;
     5.9    fun merge
    5.10     ({records = recs1,
     6.1 --- a/src/HOL/arith_data.ML	Wed Nov 28 00:44:37 2001 +0100
     6.2 +++ b/src/HOL/arith_data.ML	Wed Nov 28 00:46:26 2001 +0100
     6.3 @@ -213,7 +213,6 @@
     6.4  
     6.5    val empty = {splits = [], inj_consts = [], discrete = []};
     6.6    val copy = I;
     6.7 -  val finish = I;
     6.8    val prep_ext = I;
     6.9    fun merge ({splits= splits1, inj_consts= inj_consts1, discrete= discrete1},
    6.10               {splits= splits2, inj_consts= inj_consts2, discrete= discrete2}) =
     7.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Wed Nov 28 00:44:37 2001 +0100
     7.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Wed Nov 28 00:46:26 2001 +0100
     7.3 @@ -100,7 +100,6 @@
     7.4    val empty = {add_mono_thms = [], mult_mono_thms = [], inj_thms = [],
     7.5                 lessD = [], simpset = Simplifier.empty_ss};
     7.6    val copy = I;
     7.7 -  val finish = I;
     7.8    val prep_ext = I;
     7.9  
    7.10    fun merge ({add_mono_thms= add_mono_thms1, mult_mono_thms= mult_mono_thms1, inj_thms= inj_thms1,
     8.1 --- a/src/Provers/classical.ML	Wed Nov 28 00:44:37 2001 +0100
     8.2 +++ b/src/Provers/classical.ML	Wed Nov 28 00:46:26 2001 +0100
     8.3 @@ -922,7 +922,6 @@
     8.4  
     8.5    val empty = ref empty_cs;
     8.6    fun copy (ref cs) = (ref cs): T;            (*create new reference!*)
     8.7 -  val finish = I;
     8.8    val prep_ext = copy;
     8.9    fun merge (ref cs1, ref cs2) = ref (merge_cs (cs1, cs2));
    8.10    fun print _ (ref cs) = print_cs cs;
     9.1 --- a/src/Provers/simplifier.ML	Wed Nov 28 00:44:37 2001 +0100
     9.2 +++ b/src/Provers/simplifier.ML	Wed Nov 28 00:46:26 2001 +0100
     9.3 @@ -312,7 +312,6 @@
     9.4  
     9.5    val empty = ref empty_ss;
     9.6    fun copy (ref ss) = (ref ss): T;            (*create new reference!*)
     9.7 -  val finish = I;
     9.8    val prep_ext = copy;
     9.9    fun merge (ref ss1, ref ss2) = ref (merge_ss (ss1, ss2));
    9.10    fun print _ (ref ss) = print_ss ss;
    10.1 --- a/src/Pure/Isar/attrib.ML	Wed Nov 28 00:44:37 2001 +0100
    10.2 +++ b/src/Pure/Isar/attrib.ML	Wed Nov 28 00:46:26 2001 +0100
    10.3 @@ -56,7 +56,6 @@
    10.4  
    10.5    val empty = {space = NameSpace.empty, attrs = Symtab.empty};
    10.6    val copy = I;
    10.7 -  val finish = I;
    10.8    val prep_ext = I;
    10.9  
   10.10    fun merge ({space = space1, attrs = attrs1}, {space = space2, attrs = attrs2}) =
    11.1 --- a/src/Pure/Isar/calculation.ML	Wed Nov 28 00:44:37 2001 +0100
    11.2 +++ b/src/Pure/Isar/calculation.ML	Wed Nov 28 00:46:26 2001 +0100
    11.3 @@ -40,7 +40,6 @@
    11.4  
    11.5    val empty = NetRules.elim;
    11.6    val copy = I;
    11.7 -  val finish = I;
    11.8    val prep_ext = I;
    11.9    val merge = NetRules.merge;
   11.10    val print = print_rules Display.pretty_thm_sg;
    12.1 --- a/src/Pure/Isar/induct_attrib.ML	Wed Nov 28 00:44:37 2001 +0100
    12.2 +++ b/src/Pure/Isar/induct_attrib.ML	Wed Nov 28 00:46:26 2001 +0100
    12.3 @@ -110,7 +110,6 @@
    12.4      ((init_rules (first_var o #2), init_rules (Thm.major_prem_of o #2)),
    12.5       (init_rules (last_var o #2), init_rules (Thm.major_prem_of o #2)));
    12.6    val copy = I;
    12.7 -  val finish = I;
    12.8    val prep_ext = I;
    12.9    fun merge (((casesT1, casesS1), (inductT1, inductS1)),
   12.10        ((casesT2, casesS2), (inductT2, inductS2))) =
    13.1 --- a/src/Pure/Isar/method.ML	Wed Nov 28 00:44:37 2001 +0100
    13.2 +++ b/src/Pure/Isar/method.ML	Wed Nov 28 00:46:26 2001 +0100
    13.3 @@ -176,7 +176,6 @@
    13.4  
    13.5    val empty = [NetRules.intro, NetRules.elim, NetRules.intro, NetRules.elim];
    13.6    val copy = I;
    13.7 -  val finish = I;
    13.8    val prep_ext = I;
    13.9    fun merge x = map2 NetRules.merge x;
   13.10    val print = print_rules Display.pretty_thm_sg;
   13.11 @@ -461,7 +460,6 @@
   13.12  
   13.13    val empty = {space = NameSpace.empty, meths = Symtab.empty};
   13.14    val copy = I;
   13.15 -  val finish = I;
   13.16    val prep_ext = I;
   13.17    fun merge ({space = space1, meths = meths1}, {space = space2, meths = meths2}) =
   13.18      {space = NameSpace.merge (space1, space2),
    14.1 --- a/src/Pure/Isar/object_logic.ML	Wed Nov 28 00:44:37 2001 +0100
    14.2 +++ b/src/Pure/Isar/object_logic.ML	Wed Nov 28 00:46:26 2001 +0100
    14.3 @@ -40,7 +40,6 @@
    14.4  
    14.5    val empty = (None, ([], [Drule.norm_hhf_eq]));
    14.6    val copy = I;
    14.7 -  val finish = I;
    14.8    val prep_ext = I;
    14.9  
   14.10    fun merge_judgment (Some x, Some y) =
    15.1 --- a/src/Pure/Isar/rule_context.ML	Wed Nov 28 00:44:37 2001 +0100
    15.2 +++ b/src/Pure/Isar/rule_context.ML	Wed Nov 28 00:46:26 2001 +0100
    15.3 @@ -115,7 +115,6 @@
    15.4  
    15.5    val empty = empty_rules;
    15.6    val copy = I;
    15.7 -  val finish = I;
    15.8    val prep_ext = I;
    15.9  
   15.10    fun merge (Rules {rules = rules1, wrappers = wrappers1, ...},
    16.1 --- a/src/Pure/Thy/present.ML	Wed Nov 28 00:44:37 2001 +0100
    16.2 +++ b/src/Pure/Thy/present.ML	Wed Nov 28 00:46:26 2001 +0100
    16.3 @@ -78,7 +78,6 @@
    16.4  
    16.5    val empty = {name = "Pure", session = [], is_local = false};
    16.6    val copy = I;
    16.7 -  val finish = I;
    16.8    fun prep_ext _ = {name = "", session = [], is_local = false};
    16.9    fun merge _ = empty;
   16.10    fun print _ _ = ();
    17.1 --- a/src/Pure/axclass.ML	Wed Nov 28 00:44:37 2001 +0100
    17.2 +++ b/src/Pure/axclass.ML	Wed Nov 28 00:46:26 2001 +0100
    17.3 @@ -172,7 +172,6 @@
    17.4  
    17.5    val empty = Symtab.empty;
    17.6    val copy = I;
    17.7 -  val finish = I;
    17.8    val prep_ext = I;
    17.9    fun merge (tab1, tab2) = Symtab.merge (K true) (tab1, tab2);
   17.10  
    18.1 --- a/src/Pure/codegen.ML	Wed Nov 28 00:44:37 2001 +0100
    18.2 +++ b/src/Pure/codegen.ML	Wed Nov 28 00:46:26 2001 +0100
    18.3 @@ -82,7 +82,6 @@
    18.4  
    18.5    val empty = {codegens = [], consts = [], types = []};
    18.6    val copy = I;
    18.7 -  val finish = I;
    18.8    val prep_ext = I;
    18.9  
   18.10    fun merge ({codegens = codegens1, consts = consts1, types = types1},
    19.1 --- a/src/Pure/goals.ML	Wed Nov 28 00:44:37 2001 +0100
    19.2 +++ b/src/Pure/goals.ML	Wed Nov 28 00:46:26 2001 +0100
    19.3 @@ -192,7 +192,6 @@
    19.4  
    19.5    val empty = make_locale_data NameSpace.empty Symtab.empty (ref []);
    19.6    fun copy {space, locales, scope = ref locs} = make_locale_data space locales (ref locs);
    19.7 -  val finish = I;
    19.8    fun prep_ext {space, locales, scope = _} = make_locale_data space locales (ref []);
    19.9    fun merge ({space = space1, locales = locales1, scope = _},
   19.10      {space = space2, locales = locales2, scope = _}) =
    20.1 --- a/src/Pure/proofterm.ML	Wed Nov 28 00:44:37 2001 +0100
    20.2 +++ b/src/Pure/proofterm.ML	Wed Nov 28 00:46:26 2001 +0100
    20.3 @@ -1048,7 +1048,6 @@
    20.4  
    20.5    val empty = ([], []);
    20.6    val copy = I;
    20.7 -  val finish = I;
    20.8    val prep_ext = I;
    20.9    fun merge ((rules1, procs1), (rules2, procs2)) =
   20.10      (merge_lists rules1 rules2, merge_alists procs1 procs2);
    21.1 --- a/src/Pure/pure_thy.ML	Wed Nov 28 00:44:37 2001 +0100
    21.2 +++ b/src/Pure/pure_thy.ML	Wed Nov 28 00:46:26 2001 +0100
    21.3 @@ -83,7 +83,6 @@
    21.4  
    21.5    val empty = mk_empty ();
    21.6    fun copy (ref x) = ref x;
    21.7 -  val finish = I;
    21.8    val prep_ext = mk_empty;
    21.9    val merge = mk_empty;
   21.10  
   21.11 @@ -390,7 +389,6 @@
   21.12  
   21.13    val empty = {name = "", version = 0};
   21.14    val copy = I;
   21.15 -  val finish = I;
   21.16    val prep_ext  = I;
   21.17    fun merge _ = empty;
   21.18    fun print _ _ = ();
   21.19 @@ -424,7 +422,6 @@
   21.20  
   21.21  fun end_theory thy =
   21.22    thy
   21.23 -  |> Theory.finish
   21.24    |> Theory.add_name (get_name thy);
   21.25  
   21.26  fun checkpoint thy =
    22.1 --- a/src/Pure/theory.ML	Wed Nov 28 00:44:37 2001 +0100
    22.2 +++ b/src/Pure/theory.ML	Wed Nov 28 00:46:26 2001 +0100
    22.3 @@ -86,7 +86,6 @@
    22.4    val hide_consts: string list -> theory -> theory
    22.5    val add_name: string -> theory -> theory
    22.6    val copy: theory -> theory
    22.7 -  val finish: theory -> theory
    22.8    val prep_ext: theory -> theory
    22.9    val prep_ext_merge: theory list -> theory
   22.10    val requires: theory -> string -> string -> unit
   22.11 @@ -98,8 +97,7 @@
   22.12  sig
   22.13    include THEORY
   22.14    val init_data: Object.kind -> (Object.T * (Object.T -> Object.T) * (Object.T -> Object.T) *
   22.15 -    (Object.T -> Object.T) * (Object.T * Object.T -> Object.T) *
   22.16 -    (Sign.sg -> Object.T -> unit)) -> theory -> theory
   22.17 +    (Object.T * Object.T -> Object.T) * (Sign.sg -> Object.T -> unit)) -> theory -> theory
   22.18    val print_data: Object.kind -> theory -> unit
   22.19    val get_data: Object.kind -> (Object.T -> 'a) -> theory -> 'a
   22.20    val put_data: Object.kind -> ('a -> Object.T) -> 'a -> theory -> theory
   22.21 @@ -229,7 +227,6 @@
   22.22  val hide_consts      = curry hide_space_i Sign.constK;
   22.23  val add_name         = ext_sign Sign.add_name;
   22.24  val copy             = ext_sign (K Sign.copy) ();
   22.25 -val finish           = ext_sign (K Sign.finish) ();
   22.26  val prep_ext         = ext_sign (K Sign.prep_ext) ();
   22.27  
   22.28  
    23.1 --- a/src/Pure/theory_data.ML	Wed Nov 28 00:44:37 2001 +0100
    23.2 +++ b/src/Pure/theory_data.ML	Wed Nov 28 00:46:26 2001 +0100
    23.3 @@ -11,7 +11,6 @@
    23.4    type T
    23.5    val empty: T
    23.6    val copy: T -> T
    23.7 -  val finish: T -> T
    23.8    val prep_ext: T -> T
    23.9    val merge: T * T -> T
   23.10    val print: Sign.sg -> T -> unit
   23.11 @@ -41,7 +40,6 @@
   23.12    Theory.init_data kind
   23.13      (Data Args.empty,
   23.14        fn (Data x) => Data (Args.copy x),
   23.15 -      fn (Data x) => Data (Args.finish x),
   23.16        fn (Data x) => Data (Args.prep_ext x),
   23.17        fn (Data x1, Data x2) => Data (Args.merge (x1, x2)),
   23.18        fn sg => fn (Data x) => Args.print sg x);
    24.1 --- a/src/Sequents/prover.ML	Wed Nov 28 00:44:37 2001 +0100
    24.2 +++ b/src/Sequents/prover.ML	Wed Nov 28 00:46:26 2001 +0100
    24.3 @@ -174,7 +174,6 @@
    24.4    type T = pack ref;
    24.5    val empty = ref empty_pack
    24.6    fun copy (ref pack) = ref pack;
    24.7 -  val finish = I;
    24.8    val prep_ext = copy;
    24.9    fun merge (ref pack1, ref pack2) = ref (merge_pack (pack1, pack2));
   24.10    fun print _ (ref pack) = print_pack pack;
    25.1 --- a/src/ZF/Tools/ind_cases.ML	Wed Nov 28 00:44:37 2001 +0100
    25.2 +++ b/src/ZF/Tools/ind_cases.ML	Wed Nov 28 00:46:26 2001 +0100
    25.3 @@ -26,7 +26,6 @@
    25.4  
    25.5    val empty = Symtab.empty;
    25.6    val copy = I;
    25.7 -  val finish = I;
    25.8    val prep_ext = I;
    25.9    fun merge (tab1, tab2) = Symtab.merge (K true) (tab1, tab2);
   25.10    fun print _ _ = ();
    26.1 --- a/src/ZF/Tools/induct_tacs.ML	Wed Nov 28 00:44:37 2001 +0100
    26.2 +++ b/src/ZF/Tools/induct_tacs.ML	Wed Nov 28 00:46:26 2001 +0100
    26.3 @@ -37,7 +37,6 @@
    26.4  
    26.5    val empty = Symtab.empty;
    26.6    val copy = I;
    26.7 -  val finish = I;
    26.8    val prep_ext = I;
    26.9    val merge: T * T -> T = Symtab.merge (K true);
   26.10  
   26.11 @@ -65,7 +64,6 @@
   26.12  
   26.13    val empty = Symtab.empty
   26.14    val copy = I;
   26.15 -  val finish = I;
   26.16    val prep_ext = I
   26.17    val merge: T * T -> T = Symtab.merge (K true)
   26.18  
    27.1 --- a/src/ZF/Tools/typechk.ML	Wed Nov 28 00:44:37 2001 +0100
    27.2 +++ b/src/ZF/Tools/typechk.ML	Wed Nov 28 00:46:26 2001 +0100
    27.3 @@ -127,7 +127,6 @@
    27.4    type T = tcset ref;
    27.5    val empty = ref (TC{rules=[], net=Net.empty});
    27.6    fun copy (ref tc) = ref tc;
    27.7 -  val finish = I;
    27.8    val prep_ext = copy;
    27.9    fun merge (ref tc1, ref tc2) = ref (merge_tc (tc1, tc2));
   27.10    fun print _ (ref tc) = print_tc tc;