tuned;

--- a/src/ZF/Tools/ind_cases.ML	Wed May 12 14:52:23 2010 +0200
+++ b/src/ZF/Tools/ind_cases.ML	Wed May 12 15:23:38 2010 +0200
@@ -19,7 +19,7 @@
 
 structure IndCasesData = Theory_Data
 (
-  type T = (Proof.context -> cterm -> thm) Symtab.table;
+  type T = (Proof.context -> conv) Symtab.table;
   val empty = Symtab.empty;
   val extend = I;
   fun merge data = Symtab.merge (K true) data;