diff -r 22b256c8c9fb -r 380e9eb40db7 src/ZF/add_ind_def.ML
--- a/src/ZF/add_ind_def.ML	Thu May 04 02:01:49 1995 +0200
+++ b/src/ZF/add_ind_def.ML	Thu May 04 02:02:18 1995 +0200
@@ -45,7 +45,7 @@
   val split_eq	: thm			(*equality rule for split*)
   val fsplitI	: thm			(*intro rule for fsplit*)
   val fsplitD	: thm			(*destruct rule for fsplit*)
-  val fsplitE	: thm			(*elim rule for fsplit*)
+  val fsplitE	: thm			(*elim rule; apparently never used*)
   end;
 
 signature SU =			(** Description of a disjoint sum **)