--- a/src/HOL/equalities.ML Fri Nov 12 17:45:36 1999 +0100
+++ b/src/HOL/equalities.ML Fri Nov 12 18:16:48 1999 +0100
@@ -163,7 +163,6 @@
Goal "{u. ? x. u = f x} = range f";
by Auto_tac;
qed "full_SetCompr_eq";
-Addsimps[full_SetCompr_eq];
section "Int";