src/ZF/Tools/ind_cases.ML

--- a/src/ZF/Tools/ind_cases.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/ZF/Tools/ind_cases.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -18,13 +18,12 @@
 
 (* theory data *)
 
-structure IndCasesData = TheoryDataFun
+structure IndCasesData = Theory_Data
 (
   type T = (simpset -> cterm -> thm) Symtab.table;
   val empty = Symtab.empty;
-  val copy = I;
   val extend = I;
-  fun merge _ tabs : T = Symtab.merge (K true) tabs;
+  fun merge data = Symtab.merge (K true) data;
 );