# HG changeset patch
# User wenzelm
# Date 1207839697 -7200
# Node ID f3535afb58e8f5124eef67a3fa967df3a934906c
# Parent  e99719e70925255fb953b992a5aa54a38d49560f
tuned;

diff -r e99719e70925 -r f3535afb58e8 src/HOL/Tools/res_axioms.ML
--- 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
diff -r e99719e70925 -r f3535afb58e8 src/Pure/Isar/code_unit.ML
--- 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);
 );
 
diff -r e99719e70925 -r f3535afb58e8 src/ZF/Tools/induct_tacs.ML
--- 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 =