# HG changeset patch
# User paulson
# Date 842283203 -7200
# Node ID a4abf41134e29d1bd8e963c26b476f45f3d77a8b
# Parent  e60a230da1795001afcd311557fd0c1348cc375e
These simpsets must not use miniscoping

diff -r e60a230da179 -r a4abf41134e2 src/CCL/CCL.ML
--- 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 ***)
 
diff -r e60a230da179 -r a4abf41134e2 src/CCL/subset.ML
--- 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;