diff -r 480a1b40fdd6 -r aad13b59b8d9 src/HOL/UNITY/Project.ML
--- a/src/HOL/UNITY/Project.ML	Fri Jul 21 17:46:43 2000 +0200
+++ b/src/HOL/UNITY/Project.ML	Fri Jul 21 18:01:36 2000 +0200
@@ -32,7 +32,7 @@
 Goal "(F Join project h C G : A co B)  =  \
 \       (extend h F Join G : (C Int extend_set h A) co (extend_set h B) &  \
 \        F : A co B)";
-by (simp_tac (simpset() addsimps [Join_constrains, project_constrains]) 1);
+by (simp_tac (simpset() addsimps [project_constrains]) 1);
 by (blast_tac (claset() addIs [extend_constrains RS iffD2 RS constrains_weaken]
                         addDs [constrains_imp_subset]) 1);
 qed "Join_project_constrains";
@@ -44,7 +44,7 @@
 \     ==> (F Join project h C G : stable A)  =  \
 \         (extend h F Join G : stable (C Int extend_set h A) &  \
 \          F : stable A)";
-by (simp_tac (simpset() addsimps [Join_project_constrains]) 1);
+by (simp_tac (HOL_ss addsimps [Join_project_constrains]) 1);
 by (blast_tac (claset() addIs [constrains_weaken] addDs [constrains_Int]) 1);
 qed "Join_project_stable";
 
@@ -52,8 +52,7 @@
 Goal "extend h F Join G : extend_set h A co extend_set h B \
 \     ==> F Join project h C G : A co B";
 by (asm_full_simp_tac
-    (simpset() addsimps [project_constrains, Join_constrains, 
-			 extend_constrains]) 1);
+    (simpset() addsimps [project_constrains, extend_constrains]) 1);
 by (blast_tac (claset() addIs [constrains_weaken]
 			addDs [constrains_imp_subset]) 1);
 qed "project_constrains_I";
@@ -61,18 +60,18 @@
 Goalw [increasing_def, stable_def]
      "extend h F Join G : increasing (func o f) \
 \     ==> F Join project h C G : increasing func";
-by (asm_full_simp_tac (simpset() addsimps [project_constrains_I, 
-					   extend_set_eq_Collect]) 1);
+by (asm_full_simp_tac (simpset_of SubstAx.thy
+		 addsimps [project_constrains_I, extend_set_eq_Collect]) 1);
 qed "project_increasing_I";
 
 Goal "(F Join project h UNIV G : increasing func)  =  \
 \     (extend h F Join G : increasing (func o f))";
 by (rtac iffI 1);
 by (etac project_increasing_I 2);
-by (asm_full_simp_tac 
-    (simpset() addsimps [increasing_def, Join_project_stable]) 1);
+by (asm_full_simp_tac (simpset_of SubstAx.thy
+		         addsimps [increasing_def, Join_project_stable]) 1);
 by (auto_tac (claset(),
-	      simpset() addsimps [Join_stable, extend_set_eq_Collect,
+	      simpset() addsimps [extend_set_eq_Collect,
 				  extend_stable RS iffD1]));
 qed "Join_project_increasing";
 
@@ -80,8 +79,7 @@
 Goal "F Join project h UNIV G : A co B \
 \     ==> extend h F Join G : extend_set h A co extend_set h B";
 by (asm_full_simp_tac
-    (simpset() addsimps [project_constrains, Join_constrains, 
-			 extend_constrains]) 1);
+    (simpset() addsimps [project_constrains, extend_constrains]) 1);
 qed "project_constrains_D";
 
 
@@ -192,7 +190,7 @@
 
 Goalw [extending_def]
      "extending v (%G. UNIV) h F (increasing (func o f)) (increasing func)";
-by (simp_tac (simpset() addsimps [Join_project_increasing]) 1);
+by (simp_tac (HOL_ss addsimps [Join_project_increasing]) 1);
 qed "extending_increasing";
 
 
@@ -216,7 +214,7 @@
 Goalw [Constrains_def]
      "F Join project h (reachable (extend h F Join G)) G : A Co B  \
 \     ==> extend h F Join G : (extend_set h A) Co (extend_set h B)";
-by (full_simp_tac (simpset() addsimps [Join_project_constrains]) 1);
+by (full_simp_tac (simpset_of SubstAx.thy addsimps [Join_project_constrains]) 1);
 by (Clarify_tac 1);
 by (etac constrains_weaken 1);
 by (auto_tac (claset() addIs [reachable_imp_reachable_project], simpset()));
@@ -277,14 +275,14 @@
 Goalw [Constrains_def]
      "extend h F Join G : (extend_set h A) Co (extend_set h B)  \
 \     ==> F Join project h (reachable (extend h F Join G)) G : A Co B";
-by (full_simp_tac (simpset() addsimps [Join_project_constrains, 
+by (full_simp_tac (simpset_of SubstAx.thy addsimps [Join_project_constrains, 
 				       extend_set_Int_distrib]) 1);
 by (rtac conjI 1);
 by (force_tac
     (claset() addEs [constrains_weaken_L]
               addSDs [extend_constrains_project_set,
 		      subset_refl RS reachable_project_imp_reachable], 
-     simpset() addsimps [Join_constrains]) 2);
+     simpset()) 2);
 by (blast_tac (claset() addIs [constrains_weaken_L]) 1);
 qed "project_Constrains_I";
 
@@ -421,7 +419,7 @@
 \     ==> F Join project h C G  \
 \           : (project_set h C Int project_set h A) ensures (project_set h B)";
 by (asm_full_simp_tac
-    (simpset() addsimps [ensures_def, Join_constrains, project_constrains, 
+    (simpset() addsimps [ensures_def, project_constrains, 
 			 Join_transient, extend_transient]) 1);
 by (Clarify_tac 1);
 by (REPEAT_FIRST (rtac conjI));
@@ -463,8 +461,7 @@
                        addIs [transient_strengthen, project_set_I,
 			      project_unless RS unlessD, unlessI, 
 			      project_extend_constrains_I], 
-	      simpset() addsimps [ensures_def, Join_constrains,
-				  Join_stable, Join_transient]));
+	      simpset() addsimps [ensures_def, Join_transient]));
 qed_spec_mp "Join_project_ensures";
 
 (** Lemma useful for both STRONG and WEAK progress, but the transient
@@ -498,7 +495,7 @@
 \        F Join project h C G : A LeadsTo B |] \
 \     ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)";
 by (asm_full_simp_tac 
-    (simpset() addsimps [LeadsTo_def, project_leadsTo_D_lemma, 
+    (simpset_of SubstAx.thy addsimps [LeadsTo_def, project_leadsTo_D_lemma, 
 			 project_set_reachable_extend_eq]) 1);
 qed "Join_project_LeadsTo";
 
@@ -506,7 +503,6 @@
 (*** Towards project_Ensures_D ***)
 
 
-
 Goalw [project_set_def, extend_set_def, project_act_def]
      "act ^^ (C Int extend_set h A) <= B \
 \     ==> project_act h (Restrict C act) ^^ (project_set h C Int A) \
@@ -560,8 +556,7 @@
 (*unless*)
 by (auto_tac (claset() addSIs [rewrite_rule [unless_def] project_unless2] 
                        addIs [project_extend_constrains_I], 
-	      simpset() addsimps [ensures_def, Join_constrains,
-				  Join_stable]));
+	      simpset() addsimps [ensures_def]));
 (*transient*)
 by (auto_tac (claset(), simpset() addsimps [Join_transient]));
 by (blast_tac (claset() addIs [stable_project_transient]) 2);