# HG changeset patch
# User oheimb
# Date 942427008 -3600
# Node ID 058193827a52a1c97e484d38c8377b461c0771dd
# Parent  b7713108ffd8678f9e8125920b4309ea27f74c94
removed full_SetCompr_eq from simpset() again

diff -r b7713108ffd8 -r 058193827a52 src/HOL/equalities.ML
--- 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";