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