tuned;
authorwenzelm
Thu Apr 10 17:01:37 2008 +0200 (2008-04-10)
changeset 26618f3535afb58e8
parent 26617 e99719e70925
child 26619 c348bbe7c87d
tuned;
src/HOL/Tools/res_axioms.ML
src/Pure/Isar/code_unit.ML
src/ZF/Tools/induct_tacs.ML
     1.1 --- a/src/HOL/Tools/res_axioms.ML	Thu Apr 10 16:15:53 2008 +0200
     1.2 +++ b/src/HOL/Tools/res_axioms.ML	Thu Apr 10 17:01:37 2008 +0200
     1.3 @@ -394,11 +394,11 @@
     1.4    Skolem functions.*)
     1.5  structure ThmCache = TheoryDataFun
     1.6  (
     1.7 -  type T = (thm list) Thmtab.table;
     1.8 +  type T = thm list Thmtab.table;
     1.9    val empty = Thmtab.empty;
    1.10 -  fun copy tab : T = tab;
    1.11 -  val extend = copy;
    1.12 -  fun merge _ (tab1, tab2) : T = Thmtab.merge (K true) (tab1, tab2);
    1.13 +  val copy = I;
    1.14 +  val extend = I;
    1.15 +  fun merge _ tabs : T = Thmtab.merge (K true) tabs;
    1.16  );
    1.17  
    1.18  (*Populate the clause cache using the supplied theorem. Return the clausal form
     2.1 --- a/src/Pure/Isar/code_unit.ML	Thu Apr 10 16:15:53 2008 +0200
     2.2 +++ b/src/Pure/Isar/code_unit.ML	Thu Apr 10 17:01:37 2008 +0200
     2.3 @@ -216,7 +216,7 @@
     2.4    type T = ((string * string) * thm) list;
     2.5    val empty = [];
     2.6    val copy = I;
     2.7 -  val extend = copy;
     2.8 +  val extend = I;
     2.9    fun merge _ = Library.merge (eq_snd Thm.eq_thm_prop);
    2.10  );
    2.11  
     3.1 --- a/src/ZF/Tools/induct_tacs.ML	Thu Apr 10 16:15:53 2008 +0200
     3.2 +++ b/src/ZF/Tools/induct_tacs.ML	Thu Apr 10 17:01:37 2008 +0200
     3.3 @@ -56,7 +56,7 @@
     3.4    val empty = Symtab.empty
     3.5    val copy = I;
     3.6    val extend = I
     3.7 -  fun merge _ tabs: T = Symtab.merge (K true) tabs;
     3.8 +  fun merge _ tabs : T = Symtab.merge (K true) tabs;
     3.9  );
    3.10  
    3.11  structure DatatypeTactics : DATATYPE_TACTICS =