These simpsets must not use miniscoping

--- a/src/CCL/CCL.ML	Mon Sep 09 11:08:01 1996 +0200
+++ b/src/CCL/CCL.ML	Mon Sep 09 17:33:23 1996 +0200
@@ -10,8 +10,7 @@
 
 val ccl_data_defs = [apply_def,fix_def];
 
-val CCL_ss = FOL_ss addcongs set_congs
-                    addsimps  ([po_refl RS P_iff_T] @ mem_rews);
+val CCL_ss = set_ss addsimps [po_refl RS P_iff_T];
 
 (*** Congruence Rules ***)
 

--- a/src/CCL/subset.ML	Mon Sep 09 11:08:01 1996 +0200
+++ b/src/CCL/subset.ML	Mon Sep 09 17:33:23 1996 +0200
@@ -119,4 +119,6 @@
 
 val set_congs = [ball_cong, bex_cong, INT_cong, UN_cong];
 
-val set_ss = FOL_ss addcongs set_congs addsimps mem_rews;
+val set_ss = FOL_ss addcongs set_congs
+                    delsimps (ex_simps @ all_simps)  (*NO miniscoping*)
+		    addsimps mem_rews;