Added theorem distinct_lemma (needed for datatypes).

--- a/src/HOL/equalities.ML	Fri Jul 24 13:34:59 1998 +0200
+++ b/src/HOL/equalities.ML	Fri Jul 24 13:35:47 1998 +0200
@@ -727,6 +727,11 @@
 by (ALLGOALS Blast_tac);
 qed "Pow_insert";
 
+(** for datatypes **)
+Goal "f x ~= f y ==> x ~= y";
+by (Fast_tac 1);
+qed "distinct_lemma";
+
 
 (** Miniscoping: pushing in big Unions and Intersections **)
 local