theory data: copy;
authorwenzelm
Fri Apr 30 18:10:03 1999 +0200 (1999-04-30)
changeset 6556daa00919502b
parent 6555 17b7b88a8e3c
child 6557 d7e7532c128a
theory data: copy;
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/record_package.ML
src/Provers/classical.ML
src/Provers/simplifier.ML
src/ZF/Tools/induct_tacs.ML
src/ZF/Tools/typechk.ML
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Fri Apr 30 18:09:33 1999 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Fri Apr 30 18:10:03 1999 +0200
     1.3 @@ -86,6 +86,7 @@
     1.4    type T = datatype_info Symtab.table;
     1.5  
     1.6    val empty = Symtab.empty;
     1.7 +  val copy = 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	Fri Apr 30 18:09:33 1999 +0200
     2.2 +++ b/src/HOL/Tools/inductive_package.ML	Fri Apr 30 18:10:03 1999 +0200
     2.3 @@ -161,6 +161,7 @@
     2.4    type T = inductive_info Symtab.table;
     2.5  
     2.6    val empty = Symtab.empty;
     2.7 +  val copy = I;
     2.8    val prep_ext = I;
     2.9    val merge: T * T -> T = Symtab.merge (K true);
    2.10  
     3.1 --- a/src/HOL/Tools/record_package.ML	Fri Apr 30 18:09:33 1999 +0200
     3.2 +++ b/src/HOL/Tools/record_package.ML	Fri Apr 30 18:10:03 1999 +0200
     3.3 @@ -338,6 +338,7 @@
     3.4        (thm Symtab.table * Simplifier.simpset);          (*field split rules*)
     3.5  
     3.6    val empty = (Symtab.empty, (Symtab.empty, HOL_basic_ss));
     3.7 +  val copy = I;
     3.8    val prep_ext = I;
     3.9    fun merge ((recs1, (sps1, ss1)), (recs2, (sps2, ss2))) =
    3.10      (Symtab.merge (K true) (recs1, recs2),
     4.1 --- a/src/Provers/classical.ML	Fri Apr 30 18:09:33 1999 +0200
     4.2 +++ b/src/Provers/classical.ML	Fri Apr 30 18:10:03 1999 +0200
     4.3 @@ -31,7 +31,7 @@
     4.4    val clasetK: Object.kind
     4.5    exception ClasetData of Object.T ref
     4.6    val setup: (theory -> theory) list
     4.7 -  val fix_methods: Object.T * (Object.T -> Object.T) *
     4.8 +  val fix_methods: Object.T * (Object.T -> Object.T) * (Object.T -> Object.T) *
     4.9      (Object.T * Object.T -> Object.T) * (Sign.sg -> Object.T -> unit) -> unit
    4.10  end;
    4.11  
    4.12 @@ -181,18 +181,20 @@
    4.13    fun undef _ = raise Match;
    4.14  
    4.15    val empty_ref = ref ERROR;
    4.16 +  val copy_fn = ref (undef: Object.T -> Object.T);
    4.17    val prep_ext_fn = ref (undef: Object.T -> Object.T);
    4.18    val merge_fn = ref (undef: Object.T * Object.T -> Object.T);
    4.19    val print_fn = ref (undef: Sign.sg -> Object.T -> unit);
    4.20  
    4.21    val empty = ClasetData empty_ref;
    4.22 +  fun copy exn = ! copy_fn exn;
    4.23    fun prep_ext exn = ! prep_ext_fn exn;
    4.24    fun merge exn = ! merge_fn exn;
    4.25    fun print sg exn = ! print_fn sg exn;
    4.26  in
    4.27 -  val setup = [Theory.init_data clasetK (empty, prep_ext, merge, print)];
    4.28 -  fun fix_methods (e, ext, mrg, prt) =
    4.29 -    (empty_ref := e; prep_ext_fn := ext; merge_fn := mrg; print_fn := prt);
    4.30 +  val setup = [Theory.init_data clasetK (empty, copy, prep_ext, merge, print)];
    4.31 +  fun fix_methods (e, cp, ext, mrg, prt) =
    4.32 +    (empty_ref := e; copy_fn := cp; prep_ext_fn := ext; merge_fn := mrg; print_fn := prt);
    4.33  end;
    4.34  
    4.35  
    4.36 @@ -787,15 +789,16 @@
    4.37    val empty = CSData (ref empty_cs);
    4.38  
    4.39    (*create new references*)
    4.40 -  fun prep_ext (ClasetData (ref (CSData (ref cs)))) =
    4.41 +  fun copy (ClasetData (ref (CSData (ref cs)))) =
    4.42      ClasetData (ref (CSData (ref cs)));
    4.43 +  val prep_ext = copy;
    4.44  
    4.45    fun merge (ClasetData (ref (CSData (ref cs1))), ClasetData (ref (CSData (ref cs2)))) =
    4.46      ClasetData (ref (CSData (ref (merge_cs (cs1, cs2)))));
    4.47  
    4.48    fun print (_: Sign.sg) (ClasetData (ref (CSData (ref cs)))) = print_cs cs;
    4.49  in
    4.50 -  val _ = fix_methods (empty, prep_ext, merge, print);
    4.51 +  val _ = fix_methods (empty, copy, prep_ext, merge, print);
    4.52  end;
    4.53  
    4.54  
     5.1 --- a/src/Provers/simplifier.ML	Fri Apr 30 18:09:33 1999 +0200
     5.2 +++ b/src/Provers/simplifier.ML	Fri Apr 30 18:10:03 1999 +0200
     5.3 @@ -266,7 +266,8 @@
     5.4    type T = simpset ref;
     5.5  
     5.6    val empty = ref empty_ss;
     5.7 -  fun prep_ext (ref ss) = (ref ss): T;            (*create new reference!*)
     5.8 +  fun copy (ref ss) = (ref ss): T;            (*create new reference!*)
     5.9 +  val prep_ext = copy;
    5.10    fun merge (ref ss1, ref ss2) = ref (merge_ss (ss1, ss2));
    5.11    fun print _ (ref ss) = print_ss ss;
    5.12  end;
     6.1 --- a/src/ZF/Tools/induct_tacs.ML	Fri Apr 30 18:09:33 1999 +0200
     6.2 +++ b/src/ZF/Tools/induct_tacs.ML	Fri Apr 30 18:10:03 1999 +0200
     6.3 @@ -37,6 +37,7 @@
     6.4    type T = datatype_info Symtab.table;
     6.5  
     6.6    val empty = Symtab.empty;
     6.7 +  val copy = I;
     6.8    val prep_ext = I;
     6.9    val merge: T * T -> T = Symtab.merge (K true);
    6.10  
    6.11 @@ -63,6 +64,7 @@
    6.12    type T = constructor_info Symtab.table
    6.13  
    6.14    val empty = Symtab.empty
    6.15 +  val copy = I;
    6.16    val prep_ext = I
    6.17    val merge: T * T -> T = Symtab.merge (K true)
    6.18  
     7.1 --- a/src/ZF/Tools/typechk.ML	Fri Apr 30 18:09:33 1999 +0200
     7.2 +++ b/src/ZF/Tools/typechk.ML	Fri Apr 30 18:10:03 1999 +0200
     7.3 @@ -94,7 +94,8 @@
     7.4    val name = "ZF/type-checker";
     7.5    type T = tcset ref;
     7.6    val empty = ref (TC{rules=[], net=Net.empty});
     7.7 -  fun prep_ext (ref ss) = (ref ss): T;            (*create new reference!*)
     7.8 +  fun copy (ref tc) = ref tc;
     7.9 +  val prep_ext = copy;
    7.10    fun merge (ref tc1, ref tc2) = ref (merge_tc (tc1, tc2));
    7.11    fun print _ (ref tc) = print_tc tc;
    7.12    end;