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