tuned;

--- a/src/HOL/Tools/res_axioms.ML	Thu Apr 10 16:15:53 2008 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Thu Apr 10 17:01:37 2008 +0200
@@ -394,11 +394,11 @@
   Skolem functions.*)
 structure ThmCache = TheoryDataFun
 (
-  type T = (thm list) Thmtab.table;
+  type T = thm list Thmtab.table;
   val empty = Thmtab.empty;
-  fun copy tab : T = tab;
-  val extend = copy;
-  fun merge _ (tab1, tab2) : T = Thmtab.merge (K true) (tab1, tab2);
+  val copy = I;
+  val extend = I;
+  fun merge _ tabs : T = Thmtab.merge (K true) tabs;
 );
 
 (*Populate the clause cache using the supplied theorem. Return the clausal form

--- a/src/Pure/Isar/code_unit.ML	Thu Apr 10 16:15:53 2008 +0200
+++ b/src/Pure/Isar/code_unit.ML	Thu Apr 10 17:01:37 2008 +0200
@@ -216,7 +216,7 @@
   type T = ((string * string) * thm) list;
   val empty = [];
   val copy = I;
-  val extend = copy;
+  val extend = I;
   fun merge _ = Library.merge (eq_snd Thm.eq_thm_prop);
 );
 

--- a/src/ZF/Tools/induct_tacs.ML	Thu Apr 10 16:15:53 2008 +0200
+++ b/src/ZF/Tools/induct_tacs.ML	Thu Apr 10 17:01:37 2008 +0200
@@ -56,7 +56,7 @@
   val empty = Symtab.empty
   val copy = I;
   val extend = I
-  fun merge _ tabs: T = Symtab.merge (K true) tabs;
+  fun merge _ tabs : T = Symtab.merge (K true) tabs;
 );
 
 structure DatatypeTactics : DATATYPE_TACTICS =