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