# HG changeset patch
# User wenzelm
# Date 1273670618 -7200
# Node ID 116be5acd5a750f3530d8ebcccd9861da289f192
# Parent  6637878680b039856a68b09942ad19918668dc00
tuned;

diff -r 6637878680b0 -r 116be5acd5a7 src/ZF/Tools/ind_cases.ML
--- 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;