mods because of weak_case_cong

--- a/src/HOL/IMPP/Misc.ML	Tue Mar 28 12:28:24 2000 +0200
+++ b/src/HOL/IMPP/Misc.ML	Tue Mar 28 17:31:36 2000 +0200
@@ -13,8 +13,6 @@
 Goalw [update_def] "s[Loc Y::=s<Y>] = s";
 by (induct_tac "s" 1);
 by (simp_tac (simpset() addsimps [getlocs_def2]) 1);
-br ext 1;
-by (Simp_tac 1);
 qed "update_Loc_idem2";
 Addsimps[update_Loc_idem2];
 

--- a/src/HOL/MicroJava/J/WellForm.ML	Tue Mar 28 12:28:24 2000 +0200
+++ b/src/HOL/MicroJava/J/WellForm.ML	Tue Mar 28 17:31:36 2000 +0200
@@ -33,10 +33,7 @@
 val wf_cdecl_supD = prove_goalw thy [wf_cdecl_def] 
 "\\<And>X. \\<lbrakk>wf_cdecl wf_mb G (C, sc, r); C \\<noteq> Object\\<rbrakk> \\<Longrightarrow> \\<exists>D. sc = Some D \\<and> is_class G D" (K [
 	pair_tac "r" 1,
-	Asm_full_simp_tac 1,
-	strip_tac1 1,
-	option_case_tac 1,
-	Fast_tac 1]);
+	asm_full_simp_tac (simpset() addsplits [option.split_asm]) 1]);
 
 Goal "\\<lbrakk>wf_prog wf_mb G; (C,D)\\<in>(subcls1 G)^+\\<rbrakk> \\<Longrightarrow> \\<not>(D,C)\\<in>(subcls1 G)^+";
 by(etac tranclE 1);

--- a/src/HOL/ex/Factorization.ML	Tue Mar 28 12:28:24 2000 +0200
+++ b/src/HOL/ex/Factorization.ML	Tue Mar 28 17:31:36 2000 +0200
@@ -106,7 +106,7 @@
 Goal "nondec xs --> nondec (oinsert x xs)";
 by (induct_tac "xs" 1);
 by (case_tac "list" 2);
-by (ALLGOALS (Asm_full_simp_tac));
+by (ALLGOALS(asm_full_simp_tac (simpset()delcongs[thm"list.weak_case_cong"])));
 qed_spec_mp "nondec_oinsert";
 
 Goal "nondec (sort xs)";

--- a/src/HOLCF/IOA/ex/TrivEx.ML	Tue Mar 28 12:28:24 2000 +0200
+++ b/src/HOLCF/IOA/ex/TrivEx.ML	Tue Mar 28 17:31:36 2000 +0200
@@ -22,9 +22,8 @@
 by (rtac imp_conj_lemma 1);
 by (simp_tac (simpset() addsimps [trans_of_def,
         C_ioa_def,A_ioa_def,C_trans_def,A_trans_def])1);
+by (induct_tac "a" 1);
 by (simp_tac (simpset() addsimps [h_abs_def]) 1);
-by (induct_tac "a" 1);
-by Auto_tac;
 qed"h_abs_is_abstraction";
 
 

--- a/src/HOLCF/IOA/ex/TrivEx2.ML	Tue Mar 28 12:28:24 2000 +0200
+++ b/src/HOLCF/IOA/ex/TrivEx2.ML	Tue Mar 28 17:31:36 2000 +0200
@@ -22,9 +22,8 @@
 by (rtac imp_conj_lemma 1);
 by (simp_tac (simpset() addsimps [trans_of_def,
         C_ioa_def,A_ioa_def,C_trans_def,A_trans_def])1);
+by (induct_tac "a" 1);
 by (simp_tac (simpset() addsimps [h_abs_def]) 1);
-by (induct_tac "a" 1);
-by Auto_tac;
 qed"h_abs_is_abstraction";